| Age | Commit message (Collapse) | Author |
|---|
|
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
|
|
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
|
|
* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()
Fixes #3011
|
|
The `--force-logic` command line argument can be used to override a
logic specified in an input file or to set a logic when none is given.
Before this commit, both the `SmtEngine` and the parser were aware of
that argument. However, there were two issues if an input file didn't
specify a logic but `--force-logic` was used:
- Upon parsing `--force-logic`, the `SmtEngine` was informed about it
and set the logic to the forced logic. Then, the parser detected that
there was no `set-logic` command, so it set the logic to `ALL` and
emitted a corresponding warning. Finally, `SmtEngine::setDefaults()`
detected that `forceLogic` was set by the user and changed the logic
back to the forced logic. The warning was confusing and setting the
logic multiple times was not elegant.
- For eager bit-blasting, the logic was checked before resetting the
logic to the forced logic, so it would emit an error that eager
bit-blasting couldn't be used with the logic (which was `ALL` at that
point of the execution). This was a problem in the competition because
our runscript parses the `set-logic` command to decide on the
appropriate arguments to use and passes the logic to CVC4 via
`--force-logic`.
This commit moves the handling of `--force-logic` entirely into the
parser. The rationale for that is that this is not an API-level issue
(if you use the API you simply set the logic you want, forcing a
different logic in addition doesn't make sense) and simplifies the
handling of the option (no listeners need to be installed and the logic
is set only once). This commit also removes the option to set the logic
via `(set-option :cvc4-logic ...)` because it complicates matters (e.g.
which method of setting the logic takes precedence?). For the CVC and
the TPTP languages the commit creates a command to set the logic in
`SmtEngine` when the logic is forced in the parser instead of relying on
`SmtEngine` to figure it out itself.
|
|
|
|
This commit adds a check to make sure that the result of a `(check-sat)`
call matches the expected result set via `(set-info :status ...)`. In
doing so, it also fixes an issue where CVC4 would crash if asked for the
unsat core after setting the status to `unsat` but before calling
`(check-sat)` (see regression for concrete example). This happened
because CVC4 was storing the expected result and the computed result
both in the same variable (the expected result wasn't really being used
though). This commit keeps track of the expected result and the computed
result in separate variables to fix that issue.
|
|
When bit-blasting eagerly, we were not assigning values to the Boolean
variables in the `TheoryModel`. With eager bit-blasting, the BV SAT
solver gets all (converted) terms, including the Boolean ones, so
`EagerBitblaster::collectModelInfo()` is responsible for assigning
values to Boolean variables. However, it has only been assigning values
to bit-vector variables, which lead to wrong models. This commit fixes
the issue by asking the `CnfStream` for the Boolean variables, querying
the SAT solver for their value, and assigning them in the `TheoryModel`.
|
|
* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.
|
|
|
|
* Enable BV proofs when using and eager bitblaster
Specifically:
* Removed assertions that blocked them.
* Made sure that only bitvectors were stored in the BV const let-map
* Prevented true/false from being bit-blasted by the eager bitblaster
Also:
* uncommented "no-check-proofs" from relevant tests
* Option handler logic for BV proofs
BV eager proofs only work when minisat is the sat solver being used by
the BV theory.
Added logic to the --proof hanlder to verify this or throw an option
exception.
* Bugfix for proof options handler
I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.
* Clang-format
|
|
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
|
|
|
|
|
|
|
|
Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.
|
|
|
|
Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.
|
|
|
|
|
|
|
|
|
|
enabled (#1801)
Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.
|
|
Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).
This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.
|
|
|
|
|
|
|
|
|
|
* Change bvudiv semantics based on input language
The semantics of division by zero have changed from SMT 2.5 to SMT 2.6.
This commit sets the default options for the division semantics based on
the language version used. The input language was already kept track of
in the options, so this commit just updates the input language option
when there is a set-info command. This mirrors how the code already
deals with the output language.
Note: With this commit, set-info overwrites the option set by the user.
This is done to be consistent with the parser.
This partially fixes #1241.
* clang format
|
|
in regressions.
|
|
|
|
|
|
|
|
Modifying the travis rules so there are instances with proofs disabled.
|
|
Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed. Additionally, it fixes
a similar issue in the theory engine.
NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.
|
|
|
|
The rule `ExtractMultLeadingBit` estimated the number of leading zeros
wrong: when there were ones in the leading constant parts of the
factors, it was using the length of the non-zero part instead of the
length of the zero part. This commit includes an example for which the
previous version of the rule would cause a wrong answer.
|
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
options. Use bv2nat, int2bv as triggers. Add regressions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
cases of nonterminating rewrite-rules regressions.
|
|
* Reenable parts of bvsimple test
* Fix typo in #endif comment
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
success, nonzero error
|
|
|
|
None of these are enabled by default, so any performance impact
counts as a bug
Options added are:
--decision-threshold=N :default 0
+ ignore all nodes greater than threshold in first attempt to pick decision
--decision-use-weight bool :default false
+ use the weight nodes (locally, by looking at children) to direct recursive search
--decision-random-weight=N int :default 0
+ assign random weights to nodes between 0 and N-1 (0: disable)
--decision-weight-internal=HOW
+ computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)
Squashed commit of the following:
commit 0dbae066c19abde37092517b50f23255398539db
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri Apr 26 16:42:36 2013 -0400
contentless cleanup
commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue Apr 16 21:43:55 2013 -0400
bugfixes in usr1 auto weight computation
commit 9f039cba805bfd722466734920e758d48ae3b23e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri Mar 29 15:01:33 2013 -0400
DECISION_WEIGHT_INTERNAL_USR1
commit 744e16d514594e5f1c69b36473b03cf501d9b9d1
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed Mar 27 11:05:43 2013 -0400
split theory and decision requests
commit f379d8a821df31c74b42a7722e891abc5c944f16
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed Mar 27 09:51:58 2013 -0400
fix potential bug with threshold
commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed Feb 27 20:29:38 2013 -0500
stat bv::weightComputationTimer
commit 2ab97d063e221357d2bb017af4589105777fd5a3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sat Feb 23 17:02:43 2013 -0500
decision: option to auto compute weight of boolean structure
commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sat Feb 23 14:53:50 2013 -0500
decision: fix design to do partial explorations
* make findSplitterRec and all related helper functions' return
type trivalued, to be able to distinguish between
"partial exploration" vs "done exploration but found nothing"
* keep additional data structure to remember to what extent the
partial exploration has been completed so not to repeat it. we
can use this to make multiple passes on formula with arbritrary
order of thresholds for exploration
commit 0815991fc1b0f1d63f0e8124d4672d782e89d671
Author: lianah <lianahady@gmail.com>
Date: Fri Feb 22 17:55:40 2013 -0500
added simple node weight computation for bv.
commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed Feb 20 02:35:21 2013 -0500
--decision-use-weight, --decision-random-weight=N
commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue Feb 19 23:36:49 2013 -0500
decisionThreshold option
commit ac3579a52e452e3118ce116ff1823d6c6885544b
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue Feb 19 20:22:51 2013 -0500
DecisionWeightAttr
|
