Cleaning up ProofArray class. (#1208)

Ho Lambda Lifting (#1116)

* Do lambda lifting in term formula removal pass. Set option in SMT engine related to higher-order.

* Better documentation

Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remove non-invertible operators. Add regression. (#1222)

Move unsat core names to smt engine (#1192)

* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.

* Comment

* Pass expression names by reference.

* Update throw specifiers.

* Minor

* Switch expression names to CDMap, simplify interface for printing unsat core names.

* Revert throw specifier change.

* Minor simplifcations

Ho node manager types (#1203)

* Remove restrictions about function types

* Introduce notion of first-class type, improve assertions, add comment on equality type rule.

* Update comment

Add copyright information. (#1201)

This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.

Fix memory leak in quantifiers engine (#1219)

Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak
where d_quant_attr was not deleted when the QuantifiersEngine was
destroyed. This commit fixes the issue by turning d_quant_attr into an
std::unique_ptr.

Add skeleton of the FP theory solver (#1130)

This commit adds the skeleton of the theory solver using a dummy version of the converter (fp_converter.{h,cpp}). The converter is a class that is used to produce bit-vector expressions equivalent to floating-point ones. The commit sets up the equality engine and the infrastructure for interacting with the main theory components. The majority of this code is still agnostic to how the conversion is actually implemented / what kind of theory solver this is. This is pretty much the template code you need to write any kind of theory solver. This includes equality reasoning and so should be able to solve some basic problems.

Split term database (#1206)

* Move equality query to own file, move equality inference to quantifiers engine.

* Move quantifiers attributes out of TermDb and into QuantAttribute.

* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.

* Split term database into term util.

* Partial fix for #1205 that eliminates need for dependency in node.cpp.

* Add more references to github issues.

CBQI BV: Add inverse for more operators. (#1213)

This implements side conditions and the instantiation via word-level inversion for operators BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_UREM (Index=1), BITVECTOR_LSHR (index=0).

Fix typo in comment.

Split COPYING file, add missing licenses. (#1195)

The COPYING file now only contains the modified BSD license of CVC4 and specifies the software that is either incorporated into CVC4 or can be linked against CVC4. The copyright and license information for each software can now be found in the licenses/<software>-LICENSE.

The COPYING file has now 3 sections:

(1) modified BSD license of CVC4
(2) non-GPLv3 software that is incorporated in CVC4 or that can be linked against CVC4
(3) GPLv3 software that can be optionally linked against CVC4

Minor change to how SyGus commands are translated to SmtEngine commands. This ensures a single success is printed for synth-fun and synth-inv. (#1193)

Ho model (#1120)

* Update model construction for higher order. If HO_APPLY terms are present for a function, we use a curried (tree) model construction to avoid exponential size model representations for function definitions.

* Update comments.

* Change terminology in comment.

* Improve comments.

Allow CDHashMaps for objects without default constructors (#1092)

This is a patch, originally from mdeters/cdhashmap-default-constructibility that allows CDHashMaps to be declared for objects that don't have default constructors.

Add mkZero, mkOne and mkUmulo to bv utils. (#1200)

This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).

Ho quant util (#1119)

Quantifiers utilities for higher-order.

This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.

Also adds required options and a minor utility for implementing app completion.

Removing the throw specifier from ArrayStoreAll constructor. (#1182)

Addresses CIDS: 1457252 and 1379620.

Miscellaneous cleanup to ArrayStoreAll.

Add regression from #50 regarding "as" parsing in smt2 (#1188)

* Add regression from pull request #50, which was fixed separately in pull request #1162.

* Improve comment in regression

Add Cryptominisat and LFSC to --show-config output. (#1194)

Also removed obsolete CUDD related code.

Move sygus grammar utilities to separate file. (#1184)

* Move sygus grammar utilities to separate file.

* Minor

* Move includes

Op overload parser (#1162)

* Update parser for operator overloading.

* Improvements

* Updates

* Add assert

Add initial version of the SMTCOMP2018 run scripts (#1185)

This commit is a preparation step for removing the --thread-stack
option (and, ultimately, the dependency on Boost). It just copies the
2017 version of the scripts and changes the --fs-inst flag to
--fs-interleave, following the renaming in commit
7766f0ba088ad6d6c58ea9678477b255c9e52fee.

Unify hash functions for pairs (#1161)

CVC4 was implementing multiple, slightly different hash functions for
pairs. With pull request #1157, we have a decent generic hash function
for pairs. This commit replaces the existing hash function
implementations with a typedef of the generic hash function.

Add 5 FP kinds for partial to total fn conversion (#1128)

- Add new kinds for partially defined functions
- Print the new kinds
- Type rules for the new total kinds
- Constant folding and rewrites for the new total kinds

Address comments from PR #1164. (#1174)

Make eliminateSkolemFunctions(...) iterative and some more minor fixes.

Removing throw specifiers from SymbolTable::Implementation. (#1183)

Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished. (#1176)

The throw specifier has been moved to a comment.f

This allows for fixing several CIDs on FloatingPointEnumerator: 1457254, 1457258, 1457260, 1457269, 1457270, 1457274, and 1457275.

This also has miscellaneous formatting, documentation and const labeling improvements.

CID 1457268: Initializing CegConjecture::d_syntax_guided to false. (#1181)

Refactor check function in last call effort of non-linear extension. (#1175)

SyGuS streaming solution mode (#1131)

* Refactor conjecture class in ce guided instantiation, move to own file.  In preparation for sygus streaming mode.

* Infrastructure for streaming guards, more cleanup.

* Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup.

* More cleanup, add comments.

* Update comments

* Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter.

* Fix makefile.

* Cleanup.

* Remove unused includes.

* Minor

Move BvInverter class into separate file. (#1173)

A few updates to license files.

Add license information for GMP

Simplify representation of inversion Skolems for bv cegqi (#1164)

* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.

* Enable other regression

Initial working version of BV word-level instantiation (#1158)

* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems.

* Guard by option, minor notes.

* Minor

* Minor fixes.

* Minor

Better hash function for pairs (#1157)

CVC4 was computing hashes for pairs of objects by simply XORing the
hashes of the two objects. This commit implements a better way of
combining hashes based on the FNV-1a hash algorithm. The algorithm is
public domain.

Update symbol table to support operator overloading (#1154)

Fix output of --show-config for readline. (#1159)

cvc4 --show-config reported the wrong configuration for readline since
HAVE_LIBREADLINE is set to 0 or 1 but was checked with #ifdef.

Cegqi refactor prep bv (#1155)

* Preparing for bv instantiation, initial working version.

* Undoing bv changes to break up into smaller commit.

Improve finite model finding for recursive predicates (#1150)

* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.

* Simplifications, update comments.

Minor fixes for partial quantifier elimination. (#1147)

This forces "counterexample lemmas" (the formula B => ~phi[e] on page 23 of http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf) to be added during TheoryQuantifiers::preRegisterTerm instead of at full effort check. This is required to ensure that CVC4's partial quantifier elimination algorithm produces correct results.

Some background:

"get-qe" and "get-qe-disjunct" are commands in the SMT2 parser. Here is how they can be used:

[declarations]
[assertions A]
(get-qe (exists X F))

returns a ground formula F' such that A ^ F' and A ^ (exists X F) are equivalent.

The command "get-qe-disjunct" provides an interface for doing an incremental version of "get-qe".

[declarations]
[assertions A]
(get-qe-disjunct (exists X F))

returns a ground formula F1' such that A ^ F' implies A ^ (exists X F). It moreover has the property that if you call:

[declarations]
[assertions A]
(assert F1')
(get-qe-disjunct (exists X F))

this will give you a formula F2' where eventually:

[declarations]
[assertions A]
(assert (not (or F1' ... Fn')))
(get-qe-disjunct (exists X F))

will either return "true" or "false", for some finite n.

Here is an example that failed before this commit:

(set-logic LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (or (not (>= (+ a (* (- 1) b)) 1)) (not (>= (+ c (* (- 1) d)) 0))))
(get-qe-disjunct (exists ((x Int)) (and (> a b) (> c x) (> d x))))

This should return:

(not (or (not (>= (+ a (* (- 1) b)) 1)) (>= (+ c (* (- 1) d)) 1)))

Previously it was returning:

false

This is because the cbqi algorithm needs to assume the negation of the quantified formula we are doing qe on before it makes any decision.

The get-qe-partial feature is being requested by Cesare and Daniel Larraz for Kind2.

This improves our performance on quantified LIA/LRA:
https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
see CVC4-092617-2-fixQePartial

CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)

This implements side conditions and the instantiation via word-level inversion for operator BITVECTOR_MULT.

Add quantifiers API example, fixes #879 (#1146)

Fix seeking for buffered input (#1145)

CVC4's implementation of seek was calculating the pointer difference
between the current position in the input and the seek point to
determine how many characters to consume. This was causing problems when
ANTLR was seeking to a pointer on a line after the current line because
it would result in a big number of characters to consume because each
line is allocated separately.  This resulted in issue #1113, where CVC4
was computing a large number of characters to consume and would block
until it received all of them.  This commit fixes and simplifies the
code by simply consuming characters until the seek point is reached
without computing a count beforehand.

Fix type checking of to_real (#1127)

to_real takes a single argument as given in kinds.

Improve FP rewriter: const folding, other (#1126)

Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and GetModelCommand to nullptr. (#1142)

Fixing Cid 1172009 (#1141)

Fixing CID 1172020: Initializing CDHashMap::iterator::d_it to nullptr. (#1139)

Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)

CID 1362904: Initializing GetInstantiationsCommand::d_smtEngine to nullptr. (#1135)

Fix build for old GMP version (#1114)

Older versions of GMP in combination with newer versions of GCC and
C++11 cause errors [0]. This commit adds the necessary includes of
<cstddef>.

[0] https://gcc.gnu.org/gcc-4.9/porting_to.html

Fixing CIDs 1172012 and 1172011: Initiallzing d_exprManager to nullptr in const_iterator. (#1140)

Cegqi refactor substitutions (#1129)

This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI).

Improvements to the code:

(1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring.
(2) The terminology "has_coeff" is replaced "is_non_basic" throughout.
(3) Added the applySubstitutionToLiteral method.
(4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was).
(5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals:
x = bv2, bvmul(x,y) = bv4
Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4
(6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual).

This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
(see CVC4-092217-cegqiRefactorSubs)

Initializing BVMinisat Solver::notify to nullptr. (#1132)

Fix bug related to sort inference + subtypes. (#1125)

Fixing CID 1362917: There was a branch where d_issup was not initialized. Switching members of InstantiationEngine to uniqur_ptr to simplify such cases. (#1133)

Fixing CID 1362895: Initializing d_bvp to nullptr. (#1137)

* Fixing CID 1362895: Initializing d_bvp to nullptr. Miscellaneous cleanup.

CID 1362907: Initializing d_smtEngine to nullptr. (#1134)

Sygus inv templ refactor (#1110)

* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.

* Update comment on class

* Cleanup

* Comments for sygus type construction.

Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)

* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms.

* Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent.

* Remove unused NodeList

Fix issue #1081, memory leak in cmd executor (#1109)

The variable `g` could be set multiple times depending on
the options (e.g. a combination of `--dump-unsat-cores`
and `--dump-synth`), which could lead to memory leaks and
missing output. This commit fixes the issue by replacing
`g` with a list of `getterCommands` that are all executed and
deleted.

Add FP type enumerator and cardinality computer (#1104)

Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)

Removing a potentially invalid comparison in the TPTP parser. (#1091)

Fix issue #1074, improve non-fatal error handling (#1075)

Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.

One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.

This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.

Refactor cegqi instantiation infrastructure so that it is more independent of instantiation for LIA. (#1111)

Fix issue #1105 involving string to int (#1112)

This was introduced by changing the implementation of "isNumber" in this commit:
a94318b

This fixes issue #1105.

Floating point symfpu support (#1103)

- Update the parser to the new constant construction
- Fix the problem with parsing +/-zero and remove some dead code
- Extend the interface for literal floating-point values.
- Add a constructor so that a parameteric operator structure can be created from a type
- Add constructors so parametric operator constants can be easily converted
- Update SMT2 printing so that it uses the informative output

Moving the CVC4_PUBLIC attribute to the beginning of operator++. (#1107)

Removes the following warning when compiling with gcc version 4.8.4 :

../../../../../src/expr/kind_template.h:95:55: warning: '__visibility__' attribute ignored on non-class types [-Wattributes]

Tested with clang-3.5.

Make floating-point comparison operators chainable (#1101)

Floating-point comparison operators are chainable according to the standard.

Add missing CVC4_PUBLIC in kind_template (#1078)

Enable ccache compression, increase cache size (#1099)

This commit enables compression for ccache, increases the cache size to 1GB and
resets the ccache statistics before each run.

Remove unhandled subtypes (#1098)

* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).

* Update unit test for parametric datatypes to reflect new subtyping relation.

* Remove deprecated test.

* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).

Simplifying the throw specifier of SmtEngine::checkSat and related calls to CVC4::Exception. (#1085)

Floating point symfpu support (#1093)

Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.

Add new kinds required for higher-order. (#1083)

This consists of a binary apply symbol HO_APPLY that returns the result of applying its first argument to its second argument. Update the UF rewriter to ensure that non-standard APPLY_UF applications are rewritten into curried applications of HO_APPLY.

Add isConst check for lambda expressions. (#1084)

Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.

Make ccache work with Clang on Travis (#1097)

This commit uses a workaround [0] to get ccache to work
with Clang on Travis.

[0] https://github.com/travis-ci/travis-ci/issues/5383#issuecomment-224630584

Modify equality engine to allow operators to be marked as external terms (#1082)

This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.

This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.

This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445

Remove unused RecordSelect and TupleSelect (#1087)

Commit 62b673a6b8444c14c169a984dd6e3fc8f685851e remove most of the
record/tuple infrastructure but did not remove the classes RecordSelect and
TupleSelect which lead to issues with Java bindings (the references to the
corresponding mkConst implementations could not be resolved). This commit
removes the remaining traces of those classes.

Enable ccache on Travis, disable debug symbols (#1094)

Enable ccache on Travis for faster compile times. Also
disable debug symbols for the debug builds on Travis to
use the available cache more efficiently. Note: this
change only works on GCC, support for Clang will require
additional changes but the time savings should already be
pretty significant.

Initial infrastructure for BV instantiation via word-level inversions. (#1056)

* Initial infrastructure for BV instantiation via word-level inversions.

* Minor clean up.

* Change visited to unordered set.

Adding reasonable breaks in switch statement in TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079)

Addressing a coverity scan complaint in theory_strings.cpp. I believe the root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)

Ensure that expand definitions is called on all non-variable expressi… (#1070)

* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.

* Add comments concerning expandDefinitions

* Expand comment, move to .h

Properly handle user cardinality constraints for uf-ss=none. (#1068)

Fix link in configure.ac.

Remove support for conversions between uint32/uint16 and string. (#1069)

* Remove support for conversions between uint32/uint16 and string.

* Temporarily disable regression.

Add travis debug build with cln. (#1066)

Until now, all travis builds where built with gmp. This commit adds an additional debug build built with cln.

Add GCC7 jobs to Travis (#1054)

This commit adds two jobs (debug, with portfolio, test groups 0 and 1) to Travis.
Both jobs are added using matrix.include, based on the example in the documentation:
https://docs.travis-ci.com/user/languages/cpp/#GCC-on-Linux . This
unfortunately requires some code duplication but there does not seem to be a
way to do it in a much better fashion.

Replace CVC4_THREADLOCAL in interactive_shell (#1065)

Commit 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4
caused our nightly builds to fail because it did
not replace CVC4_THREADLOCAL with
CVC4_THREAD_LOCAL in interactive_shell. This
commit fixes the issue and adds readline to
Travis, s.t. readline related code gets compiled
as part of our CI tests.

Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060)

Use thread_local instead of compiler extensions (#210)

C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.

Fix model construction for parametric types (#1059)

Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values.

There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded).

This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet.

There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first.

The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction.

Remove Coverity SSL certificate workaround from Travis configuration. (#1058)

Coverity works without the SSL certificate workaround and is not needed anymore. Note that we don't require sudo anymore and we could switch to container-based Travis builds (instead of VM-based).  However, container-based environments only provide 4G of memory (instead of 7.5G for VMs) , which is not enough for the current CVC4 build environment.

Fix indentation for disabled Java tests.

Disable Java tests for now until they get fixed.

Run Ant on Travis