Add new infrastructure for preprocessing passes (#1053)

This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).

Fix issue 1433. (#1435)

Fix issue with mkConst/getConst of TypeConstant (#1439)

When compiling the Java bindings on macOS, the linker complained about
CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and
CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some
research, I found that the issue has been introduced by commit
36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the
-no-undefined flags resulted in the symbols in question being omitted
due to TypeConstant not being exported. This commit makes TypeConstant
CVC4_PUBLIC, which fixes the issue.

Add CEGQI BV linearization of additions and equalities over additions. (#1417)

Adds support for linearizing additions w.r.t. to a variable.

For example,

a * x + b + c * d * -x = e + x

is rewritten to

x * (a - c * d - 1) = e - b.

This also adds an additional rewriting rule x * x = x --> x < 2.

Fixed side conditions for CBQI BV, added unit tests. (#1434)

This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.

It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).

This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak

This simplifies to checking not (SC <=> exists x. s * x = t).

Document and clean datatypes rewriter (#1437)

Make collect model info return a Bool (#1421)

Fixes related to SyGuS + real arithmetic (#1432)

Add command for define-fun-rec and add to API (#1412)

Fixed time stats for MiniSat solve time. (#1431)

Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.

Remove CDChunkList (#1414)

Fix output of --show-trace-tags. (#1430)

Now prints each tag in a separate line.

Adding SyGuS grammars for rationals. (#1426)

Eliminate expand definitions from Sygus (#1425)

Fix strings rewriter for strip constant endpoint reverse direction (#1424)

Fix side condition for BITVECTOR_MULT. (#1422)

Normalize grammars - 2 (#1420)

This is another step towards addressing #1304 and #1344. This pull request:

- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback

This lays the basis for more general linearizations.

Minor improvements to inst match generator (#1415)

Improve rewriter for string replace (#1416)

Fix reset-assertions (#1413)

This commit fixes two issues with reset-assertions:

- pending pops were not done in SmtEngine, resulting in the following
  assertion failure:

  d_userLevels.size() == 0 && d_userContext->getLevel() == 1

- all definitions were erased on reset-assertion in an SMT2 file,
  leading to errors about undefined types

Minor additions for sygus (#1419)

Refactor and generalize PBE strategies (#1410)

Fix build when Valgrind instrumentation enabled

My last commit for the Valgrind instrumentation contained a typo that
made the nightlies fail. This commit fixes the issue.

Add debugging tools for ContextMemoryManager (#1407)

This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:

--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.

--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.

Add Gaussian Elimination as a preprocessing pass for BV. (#1342)

This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.

Fixes for issue 1404 (#1409)

Remove remaining references to QuantArith (#1408)

Minor improvements and changes to defaults for cbqi bv (#1406)

This

makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.

Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default

Allows cbqiNestedQE to be used in the BV logic.

Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).

Improve caching in term formula removal (#1398)

Adding missing break statements. CID 1362756. (#1394)

Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)

Add Cryptominisat script and patches to source file distribution.

This enables building CVC4 from a source release with Cryptominisat support.

Improve the rewriter for SINE. (#1221)

Improve rewrite for string substr (#1337)

Improve trigger filter instances (#1402)

Removing throw specifiers from internal Printer hierarchy. (#1393)

Fix models for --solve-real-as-int. (#1371)

Fixes for higher-order (#1405)

(Refactor) Instantiate utility (#1387)

Implement tangent and secant planes for transcendental functions (#1401)

Ho parsing and regressions (#1350)

Converting defined functions and let expressions from Sygus grammars to lambdas (#1403)

This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed.

The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.

Sygus Lambda Grammars (#1390)

Transcendental tangent planes utilities (#1288)

Adding infrastructure for normalizing SyGuS grammars (#1397)

* minor

Using string previously computed

* adding option

* starting module for simplifying grammars

* more

* more

* fix

* fix

* fix

* fix

* fix

* removing unused command

* removing unused command

* removing unnecessary quantifier engine

* adding lambda support

* transient

* reverting changes

* starting normalization of integers

* removing unnecessary objects

* using for_each

* rebuilding given datatypes

* recrating types as given

* bug fixing

* minor

* reverting space changes

* addressing review

* addressing review

Cegqi bv remove extract terms preprocess pass (#1376)

* Preprocess extract -> concat pass for cegqi bv.

* Add sygus bench

* Fixes, infrastructure.

* Minor fixes.

* Try

* Minor

* Minor

* Document

* Format

* Improving debug messages.

* Address

* Format

* Overlapping extracts.

* Format

* Minor

* Address review.

* Format

* Comment

* Format

Initializes members of QuantInfo. Resolves CID 1362929. (#1391)

Removing an unused variable from SygusInput. Resolves CID 1362932. (#1392)

Ho instantiation (#1204)

* Higher-order instantiation.

* Add missing files.

* Document inst match generators, make collectHoVarApplyTerms iterative.

* More documentation.

* More documentation.

* More documentation.

* More documentation

* Refactoring, documentation.

* More documentation.

* Fix comment, reference issue.

* More documentation. Fix ho trigger for the changes from master.

* Minor

* More documentation.

* More documentation.

* More

* More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive.

* More

* Minor improvements to comments.

* Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator.

* Improve documentation for ho_trigger.

* Update ho trigger to not access now private member of TermDb.

* Address comments.

* Address

* Clang format

Names the Effort enum of QuantConflictFind class. (#1354)

* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043.

* Fixing a missed assertion. Fixing a few compiler warnings.

* Switching back to an enum from an enum class.

(Refactor) Document and clean single invocation partition. (#1364)

* Documenting single invocation partiion.

* More

* More encapsulation.

* More, documentation complete.

* Split to own file.

* Format

* Fully encapsulate.

* Format

* Improvements to doc.

* Format

* Address

* Format

* Missed comment

* Newline

* Address

* Format

Add random number generator. (#1370)

This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).

(Refactor) Arithmetic monomial sum (#1381)

* Add arithmetic monomial sum utility.

* Clang format

* Fix

* Address review.

* Fix missed comment.

* Format

* Fix

Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1374)

Sygus print callbacks (#1348)

* Initial infrastructure for sygus printing.

* Minor

* Minor improvements

* Format

* Minor

* Empty constructor printer.

* Format

* Minor

* Format

* Address.

Reenable some regressions, minor. (#1369)

Removes an unused variable from Theory. (#1375)

Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 and 1362931. (#1373)

Adding garbage collection for Proof objects. (#1294)

Make QEffort an enum (#1366)

* Make QEffort an enum.

* Format

* Minor

* Fix

(Refactor) Split sygus term db (#1335)

* Split explain utility, invariance tests.

* Split extended rewriter.

* Remove unused function.

* Minor

* Move generic term utilities to term_util.

* Documentation, minor.

* Make arguments private in eval invariance.

* Document

* More documentation.

* Clang format.

* Fix, improve.

* Format

* Address review.

* Address missed comment.

* Add line breaks

* Format

Clean Ceg Instantiators (#1365)

* Initial setup for preprocessing counterexample lemmas.

* Improve documentation.

* Improving documentation, infrastructure.

* Extraction -> concatentation as a preprocess step.

* Clang format

* Minor

* Make option, refactor effort levels.

* Format

* Clean

* Format

* Rename

* Format

* More

* Format

* Splitting changes.

* Format

* Revert option.

* Minor

* Format

Cleaning up exporting vectors within commands. Resolves CID 1172285 and 1172284. (#1362)

Initializes InstPropagator::d_has_relevant_inst. Resolves 1362891. (#1360)

* Initializes InstPropagator::d_has_relevant_inst. Resolves 1362891.

* Initializing to false explicitly.

Initializes RegExpOpr::d_char_start and d_char_end. (#1359)

Initializes TriggerInfo::polarity. Resolves CID 1172054. (#1358)

* Initializes TriggerInfo::polarity. Resolves CID 1172054.

* Initializing to false explicitly.

Initializes NodeTheoryPair::timestamp in the default constructor. (#1356)

(Refactor) Decouple rep set iterator and quantifiers (#1339)

* Refactoring rep set iterator, does not modify rep set externally.

* Decouple quantifiers engine and rep set iterator.

* Documentation

* Clang format

* Minor

* Minor

* More

* Format

* Address review.

* Format

* Minor

Initializing SharedTermsDatabase::d_conflictPolarity. Resolves 1172045. (#1355)

Disable sygus qe preprocessing by default (#1353)

* Disable qe preprocessing for sygus by default, add option.

* Fix bug

* Unnest one

* Format

Implement enumerator for functions. (#1243)

* Implement enumerator for functions.

* Address review.

* Minor

* Format

* Improve comment.

* Format

Argument Relevance for Synthesis Conjectures (#1311)

* Initial work on conjecture-specific symmetry breaking.

* More infrastructure, working on process term.

* Flattening.

* Process defs

* More setup

* Fixes.

* Sketching

* Generalize to inference of argument definitions.

* More, separate conjunct processing per synth function.

* Single occurrence variables.

* Assign relevance.

* Document, connecting.

* Connecting to grammar construction.

* Enabled, add regressions.

* Fix regressions.

* Clang format.

* Add regress1, minor.

* Fix

* Two passes.

* Fix

* Note

* Improve check match, make single var occurrence more conservative.

* Add regression.

* Clang format

* Minor comments

* Update regression to new option.

* Undo grammar cons changes.

* Enable irrelevant args.

* Improvements.

* Format

* Minor

Initializes CegConjectureSingleInvSol::d_root_id. (#1361)

Initializing SortInference::initialSortCount. Resolves 1172053. (#1357)

(Documentation-only) datatype.h (#1346)

* Clean and document datatype.h.

* More, make TODOs.

* More documentation

* More

* Reference issue.

* Format

* Fixes and improvements.

* Minor

* Minor

* Minor

* Fix

* Minor

* Format

Printing for higher-order (#1347)

Higher-order prep (#1338)

* Minor preparation for final higher-order merge.

* Format

 Decouple sygus term database and term database. (#1317)

* Decouple sygus term database and term database.

* Clang format

* Fix include

Add modular arithmetic operators. (#1321)

This adds functions on Integers to compute modular addition, multiplication and inverse.

This is required for the Gaussian Elimination preprocessing pass for BV.

Initializing QModelBuilder members. (#1334)

Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)

Initializing TrailHashMap::d_uniqueKeys. (#1331)

 Initialize TimerStat::d_start. (#1330)

* Initialize TimerStat::d_start.

* 0 initializing d_data.

Initializing Smt1::d_logic in all cases. This was resolved by extending the Logic enum with an UNSET value. (#1329)

Guard relevant domain computation properly, minor. (#1325)

 Removing an unused member from Tptp. Initializing members of Tptp. (#1326)

* Removing an unused member from Tptp. Initializing members of Tptp.

* Removing delcaration for myPopCharStream.

Moving the enum ArithType to partial_model. Adding a new type Unset in the enum. Always initializing VarInfo::d_type. (#1333)

Allow FORALL in quantifier elimination command (#1322)

* Allow FORALL passed as an argument to get-qe.

* Document

* Format

* Minor

Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)

Initializing NegContainsSygusInvarianceTest::d_cpbe in constructor. (#1328)

Using unique_ptr's for members of CegConjecture. (#1324)

Updates to interface for Sygus grammar construction. (#1323)

* Updates to interface for grammar construction.

* Minor

* Format

Unrecurisify rewrite solve assertion for cbqi bv (#1312)

* Unrecursify rewrite assertion for cbqi bv.

* Format

Add getValue() for Rational and Integer (GMP and CLN). (#1309)

Returns a copy of d_value to enable public access of GMP and CLN data.

Improve rewriting for string contains part 2 (#1300)

* Generalize component contains, some infrastructure.

* Length entailment, substr for component contains, int.to.str for constant can contain concat.

* Disable rewrite.

* Fix, reenable length entailment for contains.

* Clang format, minor.

* Comment

* Minor fixes and improvements for comments.

* Improvements

* Clang format

* Fixes

* Clang format

* Fix, improve.

* Format

* Fix assertion

Make higher-order a flag in logic info. (#1318)

* Make higher-order a flag in logic info.

* Format

* Minor

* Format

Suppport SAT logic (#1310)

* Support SAT logic.

* Add lustre example.

* Add to smt1 as well.

* Fix.

* Fix.

* Fix for new option.

Fix bv help message. (#1315)

Sygus clean main (#1297)

* Remove front end hack for sygus.

* Remove other hack, add sygus solution output mode.

* Clang format

* Minor

* Fix

* Minor

* Remove unused field.

(Move-only) Split quant util (#1306)

* Initial draft of splitting quant util.

* Minor

* Document recursive term builder.

* Rename file, minor.

* Clang format