Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-09-10 | Squash implementation of counterexample-guided instantiation (#2423) | Andrew Reynolds | |
2018-09-10 | Add (str.replace (str.replace y w y) y z) rewrite (#2441) | Andres Noetzli | |
2018-09-07 | Replace boost::integer_traits with std::numeric_limits. (#2439) | Mathias Preiner | |
Further, remove redundant gmp.h include in options_handler.cpp. | |||
2018-09-07 | Remove 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-06 | Refactor and document quantifiers variable elimination and conditional ↵ | Andrew Reynolds | |
splitting (#2424) | |||
2018-09-06 | Minor 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-05 | Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432) | Mathias Preiner | |
2018-09-05 | Remove printing support for sygus enumeration types (#2430) | Andrew Reynolds | |
2018-09-05 | Finer-grained inference of substitutions in incremental mode (#2403) | Andrew Reynolds | |
2018-09-05 | Extended rewriter for string equalities (#2427) | Andrew Reynolds | |
2018-09-04 | Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428) | Mathias Preiner | |
2018-09-04 | Remove 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-04 | Remove CVC3 compatibility layer (#2418) | Andres Noetzli | |
2018-09-04 | Remove unused options file (#2413) | Andres Noetzli | |
2018-09-04 | Minor improvements to theory model builder interface. (#2408) | Andrew Reynolds | |
2018-09-04 | Make quantifiers strategies exit immediately when in conflict (#2099) | Andrew Reynolds | |
2018-09-04 | Transfer ownership of learned literals from SMT engine to circuit ↵ | Aina Niemetz | |
propagator. (#2421) | |||
2018-09-04 | Fix merge mishap of #2359. | Aina Niemetz | |
2018-09-04 | Refactor ceg conjecture initialization (#2411) | Andrew Reynolds | |
2018-08-31 | Allows SAT checks of repair const to have different options (#2412) | Haniel Barbosa | |
2018-08-31 | Refactor and document alpha equivalence. (#2402) | Andrew Reynolds | |
2018-08-31 | Fix export of bound variables (#2409) | Haniel Barbosa | |
2018-08-30 | Refactor theory preprocess into preprocessing pass. (#2395) | Mathias Preiner | |
2018-08-30 | Use useBland option in FCSimplexDecisionProcedure (#2405) | Andres Noetzli | |
2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
2018-08-29 | Refactor MipLibTrick preprocessing pass. (#2359) | Mathias Preiner | |
2018-08-29 | Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370) | Tim King | |
2018-08-29 | fix bv total ops printing (#2365) | Haniel Barbosa | |
2018-08-28 | Split term canonize utility to own file and document (#2398) | Andrew Reynolds | |
2018-08-28 | Reorder circuit propagator class. | Aina Niemetz | |
2018-08-28 | Move 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-28 | Solve equalities between Boolean variables in presolve. (#2390) | Andrew Reynolds | |
2018-08-28 | Remove throw specifiers in FP type checker (#2392) | Andres Noetzli | |
2018-08-28 | Remove dead code in fp_converter (#2388) | Andres Noetzli | |
This should fix Coverity issues 1473025 and 1459599. | |||
2018-08-28 | Fix sort inference for quantified variables of interpreted types (#2393) | Andrew Reynolds | |
2018-08-27 | Address more coverity warnings (#2394) | Andrew Reynolds | |
2018-08-27 | Fix warning in sygus io. (#2391) | Andrew Reynolds | |
2018-08-27 | Remove dead code in evaluator (#2389) | Andres Noetzli | |
This should fix Coverity issue 1470214. | |||
2018-08-27 | Refactor 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-27 | New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384) | Aina Niemetz | |
…underlying type. | |||
2018-08-27 | Use 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-27 | Resolution 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. | |||
2018-08-27 | Make division chainable in the smt2 parser (#2367) | Andrew Reynolds | |
2018-08-26 | Use uniform length limit for String constants (#2381) | Andres Noetzli | |
2018-08-26 | Fix unsigned integer type issues in strings (#2380) | Andrew Reynolds | |
* Fix unsigned integer types in strings. * Format |