summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-10Cache replace skolemscacheReplSkolemsAndres Noetzli
2018-09-10Squash implementation of counterexample-guided instantiation (#2423)Andrew Reynolds
2018-09-10Add (str.replace (str.replace y w y) y z) rewrite (#2441)Andres Noetzli
2018-09-07Replace boost::integer_traits with std::numeric_limits. (#2439)Mathias Preiner
Further, remove redundant gmp.h include in options_handler.cpp.
2018-09-07Remove clock_gettime() replacement for macOS. (#2436)Mathias Preiner
Not needed anymore since macOS 10.12 introduced clock_gettime().
2018-09-07 Make isClosedEnumerable a member of TypeNode (#2434)Andrew Reynolds
2018-09-06 Further simplify and fix initialization of ce guided instantiation (#2437)Andrew Reynolds
2018-09-06Refactor and document quantifiers variable elimination and conditional ↵Andrew Reynolds
splitting (#2424)
2018-09-06Minor improvements to interface for rep set. (#2435)Andrew Reynolds
2018-09-05 More extended rewrites for strings equality (#2431)Andrew Reynolds
2018-09-05 Eliminate select over store in quantifier bodies (#2433)Andrew Reynolds
2018-09-05Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)Mathias Preiner
2018-09-05Remove printing support for sygus enumeration types (#2430)Andrew Reynolds
2018-09-05Finer-grained inference of substitutions in incremental mode (#2403)Andrew Reynolds
2018-09-05Add regex grammar to rewriter verification tests (#2426)Andres Noetzli
2018-09-05 Extended rewriter for string equalities (#2427)Andrew Reynolds
2018-09-04Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)Mathias Preiner
2018-09-04Remove redundant strings rewrite. (#2422)Andrew Reynolds
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) ) str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z ) This PR removes the above rewrite, which was implemented incorrectly and was dead code.
2018-09-04Update INSTALL instructions (#2420)Andres Noetzli
Fixes #2419. This commit adds more information about optional dependencies, updates macOS-related information, and fixes some details.
2018-09-04Remove CVC3 compatibility layer (#2418)Andres Noetzli
2018-09-04Remove unused options file (#2413)Andres Noetzli
2018-09-04Minor improvements to theory model builder interface. (#2408)Andrew Reynolds
2018-09-04Make quantifiers strategies exit immediately when in conflict (#2099)Andrew Reynolds
2018-09-04Transfer ownership of learned literals from SMT engine to circuit ↵Aina Niemetz
propagator. (#2421)
2018-09-04Fix merge mishap of #2359.Aina Niemetz
2018-09-04Refactor ceg conjecture initialization (#2411)Andrew Reynolds
2018-08-31Allows SAT checks of repair const to have different options (#2412)Haniel Barbosa
2018-08-31Refactor and document alpha equivalence. (#2402)Andrew Reynolds
2018-08-31Fix export of bound variables (#2409)Haniel Barbosa
2018-08-30Refactor theory preprocess into preprocessing pass. (#2395)Mathias Preiner
2018-08-30Use useBland option in FCSimplexDecisionProcedure (#2405)Andres Noetzli
2018-08-30Add regular expression elimination module (#2400)Andrew Reynolds
2018-08-29Refactor MipLibTrick preprocessing pass. (#2359)Mathias Preiner
2018-08-29Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)Tim King
2018-08-29fix bv total ops printing (#2365)Haniel Barbosa
2018-08-28 Split term canonize utility to own file and document (#2398)Andrew Reynolds
2018-08-28Reorder circuit propagator class.Aina Niemetz
2018-08-28Move flag needsFinish from SMT engine to circuit propagator.Aina Niemetz
2018-08-28 Fix for get constraints method in fmf-fun (#2399)Andrew Reynolds
2018-08-28Solve equalities between Boolean variables in presolve. (#2390)Andrew Reynolds
2018-08-28Remove throw specifiers in FP type checker (#2392)Andres Noetzli
2018-08-28Remove dead code in fp_converter (#2388)Andres Noetzli
This should fix Coverity issues 1473025 and 1459599.
2018-08-28Fix sort inference for quantified variables of interpreted types (#2393)Andrew Reynolds
2018-08-27 Address more coverity warnings (#2394)Andrew Reynolds
2018-08-27Fix warning in sygus io. (#2391)Andrew Reynolds
2018-08-27Remove dead code in evaluator (#2389)Andres Noetzli
This should fix Coverity issue 1470214.
2018-08-27Refactor extended rewriter, move rewrites to aggressive (#2387)Andrew Reynolds
This is work towards #2305. With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.
2018-08-27New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)Aina Niemetz
…underlying type.
2018-08-27Use std:unique_ptr instead of raw pointers in theory/bv. (#2385)Mathias Preiner
This should also fix CIDs 1465687, 1465695, 1465696, and 1465701.
2018-08-27Resolution proof: separate printing from proof (#1964)Andres Noetzli
Currently, we have an LFSCSatProof which inherits from TSatProof and implements printing the proof. The seperation is not clean (e.g. clauseName is used for printing only but is in TSatProof) and the inheritance does not add any value while making dependencies more confusing. The plan is that TSatProof becomes a self-contained part that the MiniSat implementations generate and ProofManager prints out. This commit is a first step in that direction. For SAT solvers with native capabilities for producing proofs, we would simply implement a different LFSC printer of their proof representation without changing the SAT solver itself. The inheritance would make this awkward to deal with. Additionally, the commit cleans up some unused functions and adjusts the visibility of TSatProof methods and members.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback