cvc5.git
3 years agoMark quantifier instantiations as needs justify (#5684)
Andrew Reynolds [Wed, 16 Dec 2020 21:07:55 +0000 (15:07 -0600)]
Mark quantifier instantiations as needs justify (#5684)

This avoids a solution soundness issue when disabling all NL strategies and using --nl-rlv=always.

3 years agoSimplify synth-fun printer (#5682)
Andrew Reynolds [Wed, 16 Dec 2020 20:02:58 +0000 (14:02 -0600)]
Simplify synth-fun printer (#5682)

Simplifies synth-fun printing to assume that the function-to-synthesize should be printed with the proper name and return type.

3 years agoRenamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683)
mudathirmahgoub [Wed, 16 Dec 2020 19:22:59 +0000 (13:22 -0600)]
Renamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683)

Renamed InferInfo::getAntecedant to InferInfo::getAntecedent

3 years ago(proof-new) Use bound variable manager (#5679)
Andrew Reynolds [Wed, 16 Dec 2020 16:52:26 +0000 (10:52 -0600)]
(proof-new) Use bound variable manager (#5679)

This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.

This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.

3 years agoMove ownership of term formula removal to theory preprocessor (#5670)
Andrew Reynolds [Wed, 16 Dec 2020 15:03:45 +0000 (09:03 -0600)]
Move ownership of term formula removal to theory preprocessor (#5670)

This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.

This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.

The next step will move the TheoryPreprocessor inside prop::TheoryProxy.

There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.

3 years agoUse uint64 utility when parsing tuple selectors in smt2 (#5681)
Andrew Reynolds [Wed, 16 Dec 2020 09:33:03 +0000 (03:33 -0600)]
Use uint64 utility when parsing tuple selectors in smt2 (#5681)

The smt2 parser is now 100% independent from the Expr-layer.

3 years agoMove trigger trie to own file (#5680)
Andrew Reynolds [Tue, 15 Dec 2020 23:55:06 +0000 (17:55 -0600)]
Move trigger trie to own file (#5680)

Also updates minor things to meet coding standards and makes it so that children in the trie are not dynamically allocated.

3 years agoImprovements related to quantifiers printing (#5678)
Andrew Reynolds [Tue, 15 Dec 2020 23:16:07 +0000 (17:16 -0600)]
Improvements related to quantifiers printing (#5678)

Also fixes a bug where patterns would be printed with the wrong scope (that included the bound variable list).

3 years agoProper expand definitions for sets (#5676)
Andrew Reynolds [Tue, 15 Dec 2020 21:55:38 +0000 (15:55 -0600)]
Proper expand definitions for sets (#5676)

In the new view, expandDefinitions is used for eliminating partial operators and is not called during solving, and ppRewrite is called during preprocessing.

For sets, choose is a partial operator that should be applied in expand definitions, and in ppRewrite. On the other hand, is_singleton should not be expanded in expandDefinitions since it is not a partial operator, so it should only be handled in ppRewrite.

It also removes some outdated documentation regarding expandDefinitions with universe set, which is now handled by preventing universe set from occurring in solved substitutions.

This is in preparation for refactoring check-model.

3 years agoConsolidate basic sygus utilities regarding sygus conjectures (#5421)
Andrew Reynolds [Tue, 15 Dec 2020 21:19:08 +0000 (15:19 -0600)]
Consolidate basic sygus utilities regarding sygus conjectures (#5421)

This is required for new work on generalizing CAV 2015 single invocation techniques.

It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.

3 years agoFix datatypes compute ground value (#5671)
Andrew Reynolds [Tue, 15 Dec 2020 20:49:33 +0000 (14:49 -0600)]
Fix datatypes compute ground value (#5671)

We were using the wrong cache on one call, leading to non-constant values being enumerated.

Fixes #5659, for that benchmark, CVC4 now answers "unknown".

3 years agoRemove bv divide by zero option (#5672)
Andrew Reynolds [Tue, 15 Dec 2020 20:04:27 +0000 (14:04 -0600)]
Remove bv divide by zero option (#5672)

This is required to avoid failures in the planned refactoring of check-models.

This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.

It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.

FYI @barrettcw

3 years agoAdd getters to retrieve constants from api::Term (#5677)
Gereon Kremer [Tue, 15 Dec 2020 19:09:54 +0000 (20:09 +0100)]
Add getters to retrieve constants from api::Term (#5677)

This PR adds method to obtain constant values from api::Term that are either integers or strings.

3 years ago[proof-new] Making the CDCL(T) Minisat proof producing (#5669)
Haniel Barbosa [Mon, 14 Dec 2020 23:39:58 +0000 (20:39 -0300)]
[proof-new] Making the CDCL(T) Minisat proof producing (#5669)

This closely follows the old proof code in terms of where Minisat is hooked to the SatProofManager, other than a few places like registering removed clauses and removal of redundant literals. Note that this together with the thorough handling from SatProofManager makes the new SAT proofs perceptibly more robust than the old ones.

This PR also adds some traces to better track what Minisat does.

3 years ago[proof-new] Make prop engine proof producing (#5667)
Haniel Barbosa [Mon, 14 Dec 2020 19:06:47 +0000 (16:06 -0300)]
[proof-new] Make prop engine proof producing (#5667)

3 years agoProperly implement datatype selector triggers (#5624)
Andrew Reynolds [Mon, 14 Dec 2020 17:38:04 +0000 (11:38 -0600)]
Properly implement datatype selector triggers (#5624)

This ensures that datatype selectors are properly handled as triggers in E-matching.

This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.

It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).

This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.

Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.

FYI @barrettcw

3 years ago[proof-new] Updating interfaces between prop engine and minisat (#5664)
Haniel Barbosa [Mon, 14 Dec 2020 16:14:59 +0000 (13:14 -0300)]
[proof-new] Updating interfaces between prop engine and minisat (#5664)

This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".

Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.

3 years ago(proof-new) Add bound variable manager (#5655)
Andrew Reynolds [Mon, 14 Dec 2020 15:39:13 +0000 (09:39 -0600)]
(proof-new) Add bound variable manager (#5655)

This is a common utility for constructing canonical bound variables.

3 years agoFix and improve evaluator (#5563)
Andrew Reynolds [Mon, 14 Dec 2020 14:35:28 +0000 (08:35 -0600)]
Fix and improve evaluator (#5563)

This fixes a segfault in the evaluator for substitutions of the form x -> t where t is not constant.

This consolidates 2 cases where we did not evaluate children (when we are variable or are an application term with an unevaluated child). This was problematic previously since we would access children of currNode instead of currNodeVal.

This also makes our handling of APPLY_UF more consistent, so that it is added to the main switch statement.

3 years agoFix SAT-context dependent issue in strings preregistration (#5564)
Andrew Reynolds [Mon, 14 Dec 2020 13:04:17 +0000 (07:04 -0600)]
Fix SAT-context dependent issue in strings preregistration (#5564)

This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.

Fixes #5547.

This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.

It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.

I will do performance testing on this PR.

3 years agoFlush statistics through NodeManager in SmtEngine (#5652)
Andrew Reynolds [Sat, 12 Dec 2020 04:54:50 +0000 (22:54 -0600)]
Flush statistics through NodeManager in SmtEngine (#5652)

This removes the dependency on the Expr layer from src/main.

This requires moving the flushing of NodeManager statistics within SmtEngine.

This is a temporary solution until we have a permanent solution for statistics.

3 years agobv-to-int: new tests from an issue (#5654)
yoni206 [Fri, 11 Dec 2020 23:08:23 +0000 (15:08 -0800)]
bv-to-int: new tests from an issue (#5654)

#5293 pointed to assertion failures when employing --bv-to-int, starting from commit 94e3d9a.
The bug is not reproduced on current master, and so we would have this PR close #5293 .
This PR adds the benchmarks from #5293 .

3 years ago [proof-new] Updating theory proxy to new proof infrastructure (#5653)
Haniel Barbosa [Fri, 11 Dec 2020 21:58:13 +0000 (18:58 -0300)]
 [proof-new] Updating theory proxy to new proof infrastructure (#5653)

3 years agoFix length assumption for deq norm emp rule (#5623)
Andrew Reynolds [Fri, 11 Dec 2020 21:04:35 +0000 (15:04 -0600)]
Fix length assumption for deq norm emp rule (#5623)

There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.

Fixes #5611.

Note this inference was not previously covered in our coverage build.

3 years agoRefactor KindMap (#5646)
Gereon Kremer [Thu, 10 Dec 2020 18:53:00 +0000 (19:53 +0100)]
Refactor KindMap (#5646)

The KindMap class is only used in the EqualityEngine and implements way more than necessary.
This PR removes all the functionality that is never used.

3 years agogoogle test: expr: Migrate node_algorithm_black. (#5643)
Aina Niemetz [Thu, 10 Dec 2020 15:47:43 +0000 (07:47 -0800)]
google test: expr: Migrate node_algorithm_black. (#5643)

3 years agoRefactor regressions (#5639)
Andrew Reynolds [Thu, 10 Dec 2020 15:09:05 +0000 (09:09 -0600)]
Refactor regressions (#5639)

This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.

It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).

3 years agogoogle test: expr: Migrate kind_black. (#5634)
Aina Niemetz [Thu, 10 Dec 2020 14:11:43 +0000 (06:11 -0800)]
google test: expr: Migrate kind_black. (#5634)

3 years agoFixed a bunch of clang warnings. (#5637)
Gereon Kremer [Thu, 10 Dec 2020 00:10:36 +0000 (01:10 +0100)]
Fixed a bunch of clang warnings. (#5637)

3 years agoFix compiler warnings. (#5644)
Aina Niemetz [Wed, 9 Dec 2020 22:13:05 +0000 (14:13 -0800)]
Fix compiler warnings. (#5644)

3 years ago(proof-new) Make theory preprocessor proofs self contained (#5642)
Andrew Reynolds [Wed, 9 Dec 2020 21:00:13 +0000 (15:00 -0600)]
(proof-new) Make theory preprocessor proofs self contained (#5642)

Previously, there was a block of code in TheoryEngine::lemma for processing the proofs from theory preprocessing.

It is much cleaner if this block was self contained in TheoryPreprocessor.

This is required for the planned move of TheoryPreprocessor from TheoryEngine -> PropEngine.

3 years agogoogle test: expr: Migrate kind_map_black. (#5640)
Aina Niemetz [Wed, 9 Dec 2020 20:17:26 +0000 (12:17 -0800)]
google test: expr: Migrate kind_map_black. (#5640)

3 years agokind_map: Remove unused Accessor class. (#5641)
Aina Niemetz [Wed, 9 Dec 2020 19:44:30 +0000 (11:44 -0800)]
kind_map: Remove unused Accessor class. (#5641)

3 years agogoogle test: expr: Migrate attribute_white. (#5632)
Aina Niemetz [Wed, 9 Dec 2020 19:14:01 +0000 (11:14 -0800)]
google test: expr: Migrate attribute_white. (#5632)

3 years agoMake decision engine independent of AssertionsPipeline (#5626)
Andrew Reynolds [Wed, 9 Dec 2020 18:44:03 +0000 (12:44 -0600)]
Make decision engine independent of AssertionsPipeline (#5626)

This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.

This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.

There are no intended behavior changes in this PR.

Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).

3 years agoRemove obsolete regressions (#5633)
Andrew Reynolds [Wed, 9 Dec 2020 09:57:13 +0000 (03:57 -0600)]
Remove obsolete regressions (#5633)

This removes benchmarks for the following reasons:

- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed

3 years agogoogle test: context: Migrate context_white. (#5630)
Aina Niemetz [Wed, 9 Dec 2020 09:26:31 +0000 (01:26 -0800)]
google test: context: Migrate context_white. (#5630)

google test: context: Migrate context_white.

3 years agoSplit initial exp lemma into separate lemmas. (#5622)
Gereon Kremer [Wed, 9 Dec 2020 05:38:15 +0000 (06:38 +0100)]
Split initial exp lemma into separate lemmas. (#5622)

This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.

3 years agoDelete obsolete unit tests for Expr and ExprManager. (#5631)
Aina Niemetz [Wed, 9 Dec 2020 05:23:03 +0000 (21:23 -0800)]
Delete obsolete unit tests for Expr and ExprManager. (#5631)

This is already in preparation for removing the Expr layer.

3 years agoEnsure CEGQI is applied for parametric datatypes when applicable (#5628)
Andrew Reynolds [Wed, 9 Dec 2020 04:08:52 +0000 (22:08 -0600)]
Ensure CEGQI is applied for parametric datatypes when applicable (#5628)

Previously was a bug computing the argument types of parametric datatypes.

3 years agoDo not check FP at last call if not necessary (#5627)
Andrew Reynolds [Wed, 9 Dec 2020 01:59:51 +0000 (19:59 -0600)]
Do not check FP at last call if not necessary (#5627)

This makes the theory of floating points not request a last call effort check, if that call is known to do nothing.

This should make CVC4 (more) agnostic to whether --symfpu is enabled during configuration.

3 years agoite_utilities: Fix infinite loop in compressTerm. (#5629)
Aina Niemetz [Wed, 9 Dec 2020 01:03:49 +0000 (17:03 -0800)]
ite_utilities: Fix infinite loop in compressTerm. (#5629)

Fixes #4610.

3 years agoupdate doc (#5619)
yoni206 [Wed, 9 Dec 2020 00:42:25 +0000 (16:42 -0800)]
update doc (#5619)

The current help message for --bv-div-zero-const only mentions bvudiv (in which the result is -1) and not bvurem (in which the result is the first argument).
I think this is a bit misleading, because in practice, this option controls also the behavior of bvurem:
CVC4/src/theory/bv/theory_bv.cpp

Line 134 in 0309ef4

 if (options::bitvectorDivByZeroConst())
This PR is an attempt to provide a more accurate help message.

3 years agogoogle test: context: Migrate context_mm_black. (#5592)
Aina Niemetz [Tue, 8 Dec 2020 23:10:50 +0000 (15:10 -0800)]
google test: context: Migrate context_mm_black. (#5592)

3 years agogoogle test: context: Migrate context_black. (#5587)
Aina Niemetz [Tue, 8 Dec 2020 22:20:11 +0000 (14:20 -0800)]
google test: context: Migrate context_black. (#5587)

3 years agoAdd regression from #1978. (#5552)
Gereon Kremer [Tue, 8 Dec 2020 20:48:21 +0000 (21:48 +0100)]
Add regression from #1978. (#5552)

This PR adds a regression from #1978 that has been fixed in the meantime.
Closes #1978 .

3 years agoFix a bug with synth-fun printer (#5512)
Abdalrhman Mohamed [Tue, 8 Dec 2020 20:10:10 +0000 (14:10 -0600)]
Fix a bug with synth-fun printer (#5512)

This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.

3 years ago[proof-new] Updating SAT proof to use MACRO_RESOLUTION (#5613)
Haniel Barbosa [Tue, 8 Dec 2020 14:44:17 +0000 (11:44 -0300)]
[proof-new] Updating SAT proof to use MACRO_RESOLUTION (#5613)

3 years agobv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing...
yoni206 [Tue, 8 Dec 2020 12:51:06 +0000 (04:51 -0800)]
bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing pass (#5620)

#5544 enforces expandDefinition not to run before preprocessing.
The bv-to-int preprocessing pass used to rely on expandDefinition to replace BITVECTOR_UDIV and BITVECTOR_UREM with their _TOTAL versions.
This PR performs the replacement in the preprocessing pass itself.
A regression that timed out is now fixed and is brought back to the regressions.

3 years agoMake term indices in the strings base solver aware of types (#5589)
Andrew Reynolds [Tue, 8 Dec 2020 07:50:10 +0000 (01:50 -0600)]
Make term indices in the strings base solver aware of types (#5589)

This is required for handling inputs that combine strings and sequences.

Fixes #5542.

3 years agoProper implementation of expand definitions for sequences (#5616)
Andrew Reynolds [Tue, 8 Dec 2020 06:38:14 +0000 (00:38 -0600)]
Proper implementation of expand definitions for sequences (#5616)

Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with.

This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly.

To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation.

Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs.

3 years agoFix collect model values for sequences of sequences (#5579)
Andrew Reynolds [Tue, 8 Dec 2020 04:46:22 +0000 (22:46 -0600)]
Fix collect model values for sequences of sequences (#5579)

Fixes #5543.

Recently we changed our model construction for sequences here: #5391.

This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term.

This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues.

3 years ago[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)
Haniel Barbosa [Tue, 8 Dec 2020 03:54:11 +0000 (00:54 -0300)]
[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)

Previously CHAIN_RESOLUTION's definition and checker were not properly capturing its intended behavior as merely an n-ary RESOLUTION rule (i.e., no factoring nor reordering). A new rule, MACRO_RESOLUTION, now captures this behavior: it combines CHAIN_RESOLUTION, FACTORING, and REORDERING.

This commit also adds a proof checker for the new rule and updates the proof checker of CHAIN_RESOLUTION.

3 years agoAdd support for BV proofs with the simple bitblasting solver. (#5603)
Mathias Preiner [Tue, 8 Dec 2020 03:15:14 +0000 (19:15 -0800)]
Add support for BV proofs with the simple bitblasting solver. (#5603)

3 years agoDisable algebraic BV subtheory by default and make experimental. (#5596)
Mathias Preiner [Tue, 8 Dec 2020 02:06:30 +0000 (18:06 -0800)]
Disable algebraic BV subtheory by default and make experimental. (#5596)

Fixes #5370, #5462.

3 years agoFix and reenable fact vs lemma optimization in datatypes (#5614)
Andrew Reynolds [Mon, 7 Dec 2020 22:12:47 +0000 (16:12 -0600)]
Fix and reenable fact vs lemma optimization in datatypes (#5614)

This corrects an issue where terms internal to datatypes were not getting properly registered e.g. as part of the indices that determine the care graph, due to a context-independent cache being used (when a SAT-context-dependent one was required).

This reenables the fact vs lemma optimization in datatypes, as it is conjectured to be correct.

3 years agoAdd bitwise refinement mode for IAND (#5328)
makaimann [Mon, 7 Dec 2020 21:39:15 +0000 (13:39 -0800)]
Add bitwise refinement mode for IAND (#5328)

Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.

For example, with a 1-bit granularity, you might learn a lemma like:

((_ iand 4) x y), value = 1
  actual (2, 3) = 2
  bv-value = #b0001
  bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y)))
         (and (and true
                  (= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0)))
                  (= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0))))
        ; BITWISE_REFINE

which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.

3 years agoFix issue with free variables introduced by quantifier rewriter (#5602)
Andrew Reynolds [Mon, 7 Dec 2020 20:43:34 +0000 (14:43 -0600)]
Fix issue with free variables introduced by quantifier rewriter (#5602)

This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.

This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.

3 years agoRefactor initial phase of transcendental solver (#5599)
Gereon Kremer [Mon, 7 Dec 2020 19:59:10 +0000 (20:59 +0100)]
Refactor initial phase of transcendental solver (#5599)

This PR refactors the initialization of the transcendental solver, decoupling the setup of generic caches from initial lemmas for exponential and sine functions.

3 years agoDo not expand theory definitions at the beginning of preprocessing (#5544)
Andrew Reynolds [Mon, 7 Dec 2020 15:51:32 +0000 (09:51 -0600)]
Do not expand theory definitions at the beginning of preprocessing (#5544)

This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.

This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.

This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.

The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).

3 years ago (proof-new) Split proof ensure closed checks to own file (#5522)
Andrew Reynolds [Mon, 7 Dec 2020 13:55:30 +0000 (07:55 -0600)]
 (proof-new) Split proof ensure closed checks to own file (#5522)

Split proof ensure closed checks to own file

3 years agoAdd regression from #4927 (#5556)
Gereon Kremer [Mon, 7 Dec 2020 13:25:08 +0000 (14:25 +0100)]
Add regression from #4927 (#5556)

The error from #4927 has been fixed in the meantime, this PR adds the example as regression.
Closes #4927.

3 years agoFix bugs in getFreeVariables (#5601)
Andrew Reynolds [Mon, 7 Dec 2020 11:26:13 +0000 (05:26 -0600)]
Fix bugs in getFreeVariables (#5601)

Did not consider scopes properly, which would fail to say that formulas with escaped variables (both bound and unbound) in formula had free variables.

3 years agoChange generated options to be thread_local. (#5583)
Everett Maus [Sat, 5 Dec 2020 01:09:54 +0000 (17:09 -0800)]
Change generated options to be thread_local. (#5583)

Signed-off-by: Everett Maus <evmaus@google.com>
3 years agogoogle test: expr: Migrate attribute_black. (#5598)
Aina Niemetz [Fri, 4 Dec 2020 20:47:30 +0000 (12:47 -0800)]
google test: expr: Migrate attribute_black. (#5598)

3 years agogoogle test: context: Migrate cdo_black. (#5586)
Aina Niemetz [Fri, 4 Dec 2020 20:07:51 +0000 (12:07 -0800)]
google test: context: Migrate cdo_black. (#5586)

3 years agogoogle test: context: Migrate cdmap_white. (#5585)
Aina Niemetz [Fri, 4 Dec 2020 18:54:46 +0000 (10:54 -0800)]
google test: context: Migrate cdmap_white. (#5585)

3 years agoFix bug in hasBoundVar (#5600)
Andrew Reynolds [Fri, 4 Dec 2020 18:26:12 +0000 (12:26 -0600)]
Fix bug in hasBoundVar (#5600)

Led to issues while debugging another issue related to free variables in assumptions.

3 years agogoogle test: api: Migrate sort_black. (#5594)
Aina Niemetz [Fri, 4 Dec 2020 16:54:32 +0000 (08:54 -0800)]
google test: api: Migrate sort_black. (#5594)

3 years agogoogle test: context: Migrate cdmap_black. (#5584)
Aina Niemetz [Fri, 4 Dec 2020 16:16:37 +0000 (08:16 -0800)]
google test: context: Migrate cdmap_black. (#5584)

3 years agogoogle test: context: Migrate cdlist_black. (#5582)
Aina Niemetz [Fri, 4 Dec 2020 15:07:22 +0000 (07:07 -0800)]
google test: context: Migrate cdlist_black. (#5582)

3 years agoUse NodeDfsIterable for makeBinary (#5595)
Alex Ozdemir [Fri, 4 Dec 2020 07:42:34 +0000 (23:42 -0800)]
Use NodeDfsIterable for makeBinary (#5595)

Replaces the manual dag traversal in BVToInt::makeBinarywith NodeDfsIterable.

This is a subset of the changes in #4176, updated to apply to master.

3 years agoupdate-copyright: Preserve file permissions. (#5597)
Mathias Preiner [Fri, 4 Dec 2020 06:32:17 +0000 (22:32 -0800)]
update-copyright: Preserve file permissions. (#5597)

When updating the copyright headers file permissions were not preserved. In some cases this results in losing the permission to execute scripts. This commit makes sure to preserve the file permissions for updated files.

3 years ago(proof-new) Updates to SMT proof manager and SmtEngine (#5446)
Andrew Reynolds [Thu, 3 Dec 2020 22:14:59 +0000 (16:14 -0600)]
(proof-new) Updates to SMT proof manager and SmtEngine (#5446)

This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode.

This makes it so that it only remains to make PropEngine to be proof producing.

3 years agogoogle test: api: Migrate solver_black. (#5570)
Aina Niemetz [Thu, 3 Dec 2020 21:29:48 +0000 (13:29 -0800)]
google test: api: Migrate solver_black. (#5570)

3 years agoUse mkAnd where the number of children may be less than two. (#5551)
Gereon Kremer [Thu, 3 Dec 2020 20:55:16 +0000 (21:55 +0100)]
Use mkAnd where the number of children may be less than two. (#5551)

An AND was constructed from a vector that may only hold a single or no element.
This PR uses mkAnd instead.
Fixes #5550 .

3 years agoModels as (#5581)
yoni206 [Thu, 3 Dec 2020 20:18:10 +0000 (12:18 -0800)]
Models as (#5581)

This PR relates to #4987 .
Our plan is to:

delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.

3 years agogoogle test: Add fixture for context tests. (#5590)
Aina Niemetz [Thu, 3 Dec 2020 19:29:58 +0000 (11:29 -0800)]
google test: Add fixture for context tests. (#5590)

Context test PRs will be updated to use this after this is merged to
master.

3 years agoRefactor handling of global declarations (#5577)
Andrew Reynolds [Thu, 3 Dec 2020 16:49:08 +0000 (10:49 -0600)]
Refactor handling of global declarations (#5577)

This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally.

This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API.

This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring.

This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now.

3 years agoMake run_regression.py executable. (#5588)
Gereon Kremer [Thu, 3 Dec 2020 15:58:48 +0000 (16:58 +0100)]
Make run_regression.py executable. (#5588)

3 years agoUpdate copyright headers.
Aina Niemetz [Thu, 3 Dec 2020 03:55:00 +0000 (19:55 -0800)]
Update copyright headers.

3 years agogoogle test: base: Migrate map_util_black. (#5580)
Aina Niemetz [Thu, 3 Dec 2020 00:37:26 +0000 (16:37 -0800)]
google test: base: Migrate map_util_black. (#5580)

3 years agoFix RoundingMode mapping in API. (#5578)
Aina Niemetz [Wed, 2 Dec 2020 23:34:13 +0000 (15:34 -0800)]
Fix RoundingMode mapping in API. (#5578)

Fixes #5524.

3 years agoRemove Record object and convert to Node-level API (#5575)
Andrew Reynolds [Wed, 2 Dec 2020 22:59:11 +0000 (16:59 -0600)]
Remove Record object and convert to Node-level API (#5575)

Required for detangling NodeManager from the Expr layer.

3 years agoRename macro Message to CVC4Message. (#5576)
Aina Niemetz [Wed, 2 Dec 2020 22:24:52 +0000 (14:24 -0800)]
Rename macro Message to CVC4Message. (#5576)

3 years agoRemove dagification visitor (#5574)
Andrew Reynolds [Wed, 2 Dec 2020 22:09:28 +0000 (16:09 -0600)]
Remove dagification visitor (#5574)

This has fully been replaced by the new let binding.

3 years agogoogle test: api: Migrate term_black. (#5571)
Aina Niemetz [Wed, 2 Dec 2020 21:55:19 +0000 (13:55 -0800)]
google test: api: Migrate term_black. (#5571)

3 years agogoogle test: api: Use individual fixture for datatype_black. (#5568)
Aina Niemetz [Wed, 2 Dec 2020 20:51:06 +0000 (12:51 -0800)]
google test: api: Use individual fixture for datatype_black. (#5568)

This is to prevent name clashes with other tests.

3 years agoAdd associative utilities to node manager (#5530)
Andrew Reynolds [Wed, 2 Dec 2020 19:03:54 +0000 (13:03 -0600)]
Add associative utilities to node manager (#5530)

Required for updating the new API to use Node utilites as backend.

These utilities are copied directly from ExprManager and converted Expr -> Node.

3 years agogoogle test: api: Migrate op_black. (#5567)
Aina Niemetz [Wed, 2 Dec 2020 18:13:54 +0000 (10:13 -0800)]
google test: api: Migrate op_black. (#5567)

3 years agogoogle test: api: Migrate grammar_black. (#5566)
Aina Niemetz [Wed, 2 Dec 2020 17:13:34 +0000 (09:13 -0800)]
google test: api: Migrate grammar_black. (#5566)

3 years agoUse new let binding for cvc printer (#5561)
Andrew Reynolds [Wed, 2 Dec 2020 16:17:09 +0000 (10:17 -0600)]
Use new let binding for cvc printer (#5561)

Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used.

3 years ago(proof-new) Proofs for expand definitions (#5562)
Andrew Reynolds [Wed, 2 Dec 2020 15:41:31 +0000 (09:41 -0600)]
(proof-new) Proofs for expand definitions (#5562)

3 years agoAdd regressions from #3687. (#5553)
Gereon Kremer [Wed, 2 Dec 2020 05:22:56 +0000 (06:22 +0100)]
Add regressions from #3687. (#5553)

The error from #3687 has been fixed in the meantime.
This PR adds the two examples from this issue as regressions.
Closes #3687

3 years agogoogle test: api: Migrate result_black. (#5569)
Aina Niemetz [Wed, 2 Dec 2020 02:24:21 +0000 (18:24 -0800)]
google test: api: Migrate result_black. (#5569)

google test: api: Migrate result_black.

3 years agoRemove use of this-> in FP literal. (#5565)
Aina Niemetz [Wed, 2 Dec 2020 02:05:27 +0000 (18:05 -0800)]
Remove use of this-> in FP literal. (#5565)

3 years agoRemove assertion related to CEGQI dependency lemmas (#5559)
Andrew Reynolds [Wed, 2 Dec 2020 01:12:01 +0000 (19:12 -0600)]
Remove assertion related to CEGQI dependency lemmas (#5559)

This assertion does not hold when we mix --sygus-inst with normal CEGQI.

Should fix the nightlies.

3 years agogoogle test: Infrastructure and first api test. (#5548)
Aina Niemetz [Wed, 2 Dec 2020 00:30:33 +0000 (16:30 -0800)]
google test: Infrastructure and first api test. (#5548)

This sets up the infrastructure for migrating unit tests from CxxTest to
Google Test. It further migrates api/datatype_api_black to the new
infrastructure.

3 years agoFix issues related to model declarations (#5560)
Andrew Reynolds [Wed, 2 Dec 2020 00:00:49 +0000 (18:00 -0600)]
Fix issues related to model declarations (#5560)

This corrects two issues related to model declarations:
(1) model declaration terms were mistaken not cleared,
(2) the model needs to be explicitly destructed before the node manager because it contains references to Node.

Fixes #5540

3 years agoImprove rewriting of str.<= (#4848)
Andres Noetzli [Tue, 1 Dec 2020 16:58:06 +0000 (08:58 -0800)]
Improve rewriting of str.<= (#4848)

This commit improves our rewriting of str.<= slightly. If we have
constant prefixes that are different, we can always rewrite the term to
a constant. Previously, we were only doing so when the result was
false.