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

(Refactor) Split term util (#1303)

* Fix some documentation.

* Move model basis out of term db.

* Moving

* Finished moving.

* Document Skolemize and term enumeration.

* Minor

* Model basis to first order model.

* Change function name.

* Minor

* Clang format.

* Minor

* Format

* Minor

* Format

* Address review.

CBQI BV choice expressions (#1296)

* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.

* Minor

* Make unique bound variables for choice functions in BvInstantor, clean up.

* Incorporate missing optimizations

* Clang format

* Unused field.

* Minor

* Fix, add regression.

* Fix regression.

* Fix bug that led to incorrect cleanup of instantiations.

* Add missing regression

* Improve handling of choice rewriting.

* Fix

* Clang format

* Use canonical variables for choice functions in cbqi bv.

* Add regression

* Clang format.

* Address review.

* Clang format

 Add option to build shared Windows dependencies (#1282)

This commit adds an option to the contrib/get-win-dependencies script
(-s) to build shared library versions of ANTLR and GMP, which enables
building the shared versions of the CVC4 libraries needed for language
bindings.

(Move-only) Refactor and document theory model part 2 (#1305)

* Move type set to its own file and document.

* Move theory engine model builder to its own class.

* Working on documentation.

* Document Theory Model.

* Minor

* Document theory model builder.

* Clang format

* Address review.

CID 1459592: Always checking whether rd is null or not. (#1299)

Remove include (#1298)

Change bvudiv semantics based on input language (#1292)

* 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

(Move only) Move enumerative instantiation strategy to its own file and document (#1290)

* Move, document, and rename enumerative instantiation.

* Clang format.

Sygus process conjecture (#1286)

* Initial infrastructure for static preprocessing for sygus conjectures.

* Initial infrastructure.

* Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest.

* Clang format

* Fixing comments, more initial infrastructure.

* More

* Minor

* New clang format.

* Address review.

Document term db (#1220)

* Document TermDb and related classes. Minor changes to quantifiers utils and their interface.  Address some comments left over from PR 1206.

* Minor

* Minor

* Change namespace style.

* Address review

* Fix incorrectly merged portion that led to regression failures.

* New clang format, fully document relevant domain.

* Clang format again.

* Minor

Improve strings rewriter for contains (#1207)

* Work on rewriter for string contains.

* Add rewrites that mix str.to.int and str.contains. Documentation, add regression.

* Minor

* Minor

* Address review, add a few TODOs. Improve some non-digit -> not is number.

* Fix

* Simplify.

* Clang format, minor fixing of comments.

Document quant arith (#1271)

* Initial documentation, incomplete.

* Document arith utilities in quantifiers.

* Minor

* Clang format

* Minor

* Clang format.

* Minor

* Apply new clang format.

* Document ordering.

Modify LDFLAGS to support shared libraries for Win  (#1280)

* Use uintptr_t for pointer casts in Swig files

CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.

* Modify LDFLAGS to support shared libraries for Win

This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which
is required for building DLLs (shared libraries on Windows). It also
adds "--export-all-symbols" to the linker flags of the parser to ensure
that there are no unresolved symbols when linking against it (see
comment in the Makefile.am for details).

* Fix for non-Windows builds

* add no-undefined to libcvc4compatjni

Cbqi multiple instantiation (#1289)

* Multi-instantiation heuristic for cbqi bv.

* New clang format.

* Minor

* Minor.

* Minor

Refactor theory model (#1236)

* Refactor theory model, working on making RepSet references const.

* Encapsulation of members of rep set.

* More documentation on rep set.

* Swap names

* Reference issues.

* Minor

* Minor

* New clang format.

Implement Hilbert choice operator (#1291)

* Initial support for Hilbert choice operator.

* Clang format.

* Fix

* Minor

Adds a macro to SWIG to ignore the override and final C++11 keywords in older versions of SWIG. (#1281)

Op overload no fun variant (#1285)

* Do not allow function variants with operator overloading.

* Minor.

* New clang format.

* Minor improvements.

Use uintptr_t for pointer casts in Swig files (#1278)

CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.

Removing throw specifiers from OutputChannel and subclasses. (#1209)

Switching EqProof to use shared_ptr everywhere.  (#1217)

This clarifies the memory ownership of EqProofs.

CBQI BV: Add handling for missing operators. (#1274)

This adds inverse handling for BITVECTOR_XOR, BITVECTOR_SIGN_EXTENDS, BITVECTOR_COMP, BITVECTOR_ASHR. Function isInvertible() now corresponds to exactly the operators (plus index) for which we can determine an inverse, which avoids traversing along non-invertible paths.

This further enables a test case that I missed to enable in PR #1268.

Cbqi bv ineq mode (#1273)

* Add mode for cbqi bv inequality handling.

* Implement the mode.

* Clang format

* Apply new clang format.

* Revert "Apply new clang format."

This reverts commit 1fec0ed999e45daacc4c756f11b5ecb4690f6561.

* Revert "Clang format"

This reverts commit 17042edb82d64c159aeddfe0264cd663998d0471.

* Clang format, second try.

* Revert "Clang format, second try."

This reverts commit f862c47c34bc313f5bc49a26b7586a4824e5aae0.

* Apply clang format, try 3.

Removing deprecated file. (#1270)

Remove clang-format options introduced in version 5.0.

New clang-format style based on the Google style. (#1264)

CBQI BV: Add ULT/SLT inverse handling. (#1268)

This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.

Document sygus programming-by-examples utility (#1260)

* Initial documentation and clean up of SyGuS PBE class, fix issue with concat strategy.

* More documentation, cleanup.

* Do not use concat strategy for 3+ arguments to concat, add regression.

* Minor

Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)

Simplify atoms introduced while bitblasting. (#1267)

If a newly introduced atom is not rewritten it can happen that the
literals of both the original atom and the rewritten atom end up in the CNF.
However, only the original atom has a BB definition and the literal of the
rewritten atom is unconstrained (no BB definition).

SyGuS term size limit (#1262)

* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.

* Apply clang format.

Make Sygus conjectures higher-order (#1244)

* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.

* Minor fix

* Fix bug in Node::hasBoundVar for non-ground operators.

* Add regression.

* Address review.

* Apply clang format.

CBQI BV: Refactor solve_bv_constraint. (#1265)

This refactors function solve_bv_constraint to use a switch-case over kinds rather than an if-else chain.

Tptp unsat cores (#1228)

* Support unsat cores for TPTP.

* Fix assertion

Strings API escape sequences (#1245)

* Argument for strings class to specify whether to process escape sequences.

* Change default value on string constructor.

* Make CVC4::String::toString symmetric to the constructor for CVC4::String, document.

* Clang format.

Making the values argument const in the SetUserAttributeCommand const… (#1249)

* Making the values argument const in the SetUserAttributeCommand constructor. Misc. cleanup of SetUserAttributeCommand.
* Removing override keyword that was making SWIG unhappy.

Fixing 2 instances of an unused variable. (#1253)

Fix for issue 1247 (#1257)

* Fix for bug 1247: in incremental mode, there was a corner case where
a skolem variable introduced during ITE removal became a solved-for
variable (part of the substitution map).  But then if the same skolem
was introduced again as part of a subsequent ITE removal pass, the
substitution was not properly applied and an incorrect result was obtained.
The handling of substitutions in incremental mode is quite kludgey - I
opened an issue to revisit this.

* fixing regression

Sygus enumerators to conjecture (#1237)

* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking.

* Change function names, simplify.

* Fix assertion, minor optimization

* Cleanup, documentation, simplification.

* Address review.

* Apply clang format.

Adds unit test that show Node and TNode work with for each loops. (#1230)

Extends test/unit/expr/node_black.h with tests that show Node and TNode can work with C++11 for each loops.

CBQI BV: Added EXTRACT handling. (#1240)

This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.

CBQI BV quick heuristics (#1239)

Adds two heuristics for cbqi-bv, both disabled by default.

The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.

Initial support for solving bit-vector inequalities (#1229)

* Initial support for solving bit-vector inequalities in cegqi-bv using conversion to positive equality + model value slack.

* Clang format, remove heuristic.

* Update regressions.

* Simplify interface for CegInstantiator