Bvlogic #601
Draft
Bvlogic #601
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
BritikovKI
force-pushed
the
bvlogic
branch
2 times, most recently
from
23bdeb3
to
eea92e1
Compare
Logic: Helpers for creating indexed terms Throw an API exception if user attempts to create an equality between different sorts smtsolver: relativelty small cleanup smtsolver: Implement a cnf clause printer bitvectors: Construct bitvector sorts and constants
fsbvlogic: Fix printing of bv constants fsbv: Renamed functions, implemented some bit blasting. fsbv: insert formula to the simplified formula root. Not sure if this is the correct way for incremental solving, but we'll see later. fsbv: Fixed the constant blasting fsbv: removed an unnecessary id string fsbv: Updated the regression tests fsbv: some comments
Overload correclty insertTerm in FSBVLogic counting: format suggestion bitblasting: Store the bitvector terms for later fetching, e.g., for counting models counting: Refactor counting code to a separate MainCounter instance. [WiP] counting: Tuning the format Interpret: added a counting command to language counting: Build an interface for interpret counting: Further tuning the format counting: Allow redirecting the counting cnf to a file counting: Generate ind line correctly
Parser: remove an unused nonterminal CMake: install SMTSolver.h ModelCounter: Fix builds MainSolver: Remove reference to model counting
BitVector counting: rewriter-based bit blaster BitVector counting: Add a missing include BitVector counting: Set vector size correctly in some places BitVectors: Determine sorts BitVectors: Remove error-prone and unnecessary sort caching BitVector counting: add a more complex example BitVectors: Fix a regression test
Interpret: Improve error reporting counting-examples: counting union of models Counting: handle correctly optimised variables In case all boolean atoms corresponding to a term that should be counted are optimised away, the code in principle correctly adds phony boolean atoms to the counting line. However, the code incorrectly searches for the boolean atoms based on the missing term. This results in an assertion failure (access to a nonexisting element in a map). This commit fixes the issue by simply adding a check that the term exists before accessing it.
BitVector: minor cleanup BitVector: Implement concat UnitTest: bitvector concatenation BitVector: Implement bvneg bvneg is implemented as (~b)+1 where ~ is the flip operation. FSBVLogic therefore has a new operator (unavaiable through the smtlib interface) bvflip. BitVector: implement bvnot UnitTest: Test for bvnot UnitTest: test for bvflip UnitTest: test for bitvector negation Bitvector: Implement `bvand` UnitTest: test for bitvector and Bitvector: Implement `bvor` UnitTest: Test for bitvector or Bitvector: implement udiv Bitvector: Update license UnitTest: tests for udiv BitVector: implement reminder UnitTest: Test for bitvector reminder Bitvector: implement left shift UnitTest: test for bitvector left shift Bitvector: Implement lshr UnitTest: test for bitvector lshr BitVectors: Fix default valules for BV sorts BitBlasting: small style fix
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This Pull Request updates and develops the Bitvector logic for the OpenSMT.