ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • df4b0ec89f Merge branch 'topic/794-kanig-cvc5' into 'master' Johannes Kanig 2024-12-18 08:38:18 +00:00
  • 2f926e4acb Disable cadical version check Johannes Kanig 2024-12-18 10:54:58 +09:00
  • 746e38e19f Fix Eunoia definition of ARRAYS_READ_OVER_WRITE_CONTRA (#11455) Andrew Reynolds 2024-12-17 14:19:02 -06:00
  • 6c11825ddf Add option to exclude tester (#11451) José Neto 2024-12-17 15:21:34 -03:00
  • fbbf9a7416 Add Eunoia definitions for 3 simple theory rewrites (#11449) Andrew Reynolds 2024-12-17 10:34:39 -06:00
  • 2e97dc2a19 Add Eunoia definitions of 3 datatype ad-hoc rewrites (#11443) Andrew Reynolds 2024-12-17 08:13:03 -06:00
  • 509d87c56f Merge cvc5 1.2.0 into AdaCore master Johannes Kanig 2024-12-17 18:48:32 +09:00
  • 8cfac8f956 Generalize elaboration for quant prenex to handle nested cases (#11450) Andrew Reynolds 2024-12-13 17:45:49 -06:00
  • d851f4fb89 theory/uf: Refactor to not use NodeManager::currentNM() (#11423) Daniel Larraz 2024-12-13 14:09:31 -06:00
  • 7075c4c3c7 Eliminate some calls to NodeManager::{currentNM,getSkolemManager} (#11436) Daniel Larraz 2024-12-13 11:27:18 -06:00
  • 1b8dd45c3a Support empty set and sequence in RARE (#11348) Andrew Reynolds 2024-12-12 18:59:32 -06:00
  • 3f41c2ab08 Add infrastructure for proofs for DIAMONDS ppStaticLearn (#11409) Andrew Reynolds 2024-12-12 18:54:48 -06:00
  • e7236b586d Refactor and extend quantifiers miniscope proof rules (#11431) Andrew Reynolds 2024-12-12 16:15:43 -06:00
  • 5716e0cd95 Add two macro rewrites for arrays (#11440) Andrew Reynolds 2024-12-12 16:02:05 -06:00
  • a149aa8d34 Update simpleRegexpConsume documentation (#11351) ofecisrael 2024-12-12 23:57:23 +02:00
  • 86bb23090d Do not handle ENCODE_EQ_INTRO in LFSC (#11439) Andrew Reynolds 2024-12-11 10:22:59 -06:00
  • 010093749b Use standard ground term skolem in quant term database (#11438) Andrew Reynolds 2024-12-11 10:12:16 -06:00
  • 4720cdfb28 Fix within-kind term context (#11437) Andrew Reynolds 2024-12-11 09:44:09 -06:00
  • cd90d14027 Update arith poly norm to handle division by constant (#11433) Andrew Reynolds 2024-12-10 18:53:11 -06:00
  • 3cc4c017d7 Move definition of ACI_NORM to own file (#11428) Andrew Reynolds 2024-12-10 18:38:53 -06:00
  • abbcf00bbb node/type_node/flatten: Eliminate calls to NodeManager::currentNM() (#11435) Daniel Larraz 2024-12-10 18:29:10 -06:00
  • 39ac796067 Replace calls to currentNM with calls to NM static methods (#11432) Daniel Larraz 2024-12-10 13:28:59 -06:00
  • 20ca3a54fd Add macro and elaboration for quantifiers prenex (#11421) Andrew Reynolds 2024-12-10 09:04:57 -06:00
  • a935292939 Fix RARE reconstruction strategy for preprocessed terms (#11416) Andrew Reynolds 2024-12-10 08:43:38 -06:00
  • e1d611385e Fix issues with alpha equivalence with quantifiers with patterns (#11418) Andrew Reynolds 2024-12-10 08:20:37 -06:00
  • 7dc4881688 Add ProofRule::ARITH_MULT_ABS_COMPARISON (#11297) Andrew Reynolds 2024-12-09 17:10:23 -06:00
  • 2a1d74a0a9 Remove NodeBuilder constructors with implicit NodeManager (#11392) Daniel Larraz 2024-12-09 15:22:44 -06:00
  • 9c1ecb0bce Fix negative pow 2 RARE rewrites for bvmul (#11417) Andrew Reynolds 2024-12-09 13:36:03 -06:00
  • f7c4876190 Fix corner case in arithmetic congruence manager proofs (#11422) Andrew Reynolds 2024-12-06 17:19:56 -06:00
  • 4d8c0800c4 Fix evaluator for prefixof in Eunoia (#11419) Andrew Reynolds 2024-12-06 17:03:38 -06:00
  • 1d50fb8ba4 Eliminate some of the calls to Node::getNodeManager (#11412) Andrew Reynolds 2024-12-06 08:33:44 -06:00
  • 6e53ea7f3b Use Minisat for configurations that are not supported with CaDiCaL. (#11410) Aina Niemetz 2024-12-05 13:29:06 -08:00
  • 6d47d158a4 Minor changes to Bool RARE rewrites (#11389) Andrew Reynolds 2024-12-05 14:06:40 -06:00
  • 83acf433a9 Handle INST_CONSTANT properly in cpc proofs (#11411) Andrew Reynolds 2024-12-05 12:00:35 -06:00
  • e8b19e748b Make macro reconstruction robust to partial failures (#11413) Andrew Reynolds 2024-12-05 10:11:18 -06:00
  • c2244f4b99 [proofs] [alethe] Remove from node converter unsupported quantifier kinds (#11414) Haniel Barbosa 2024-12-05 13:05:45 -03:00
  • a0f82efb0a Fix reconstruction for MACRO_NNF_NORM (#11408) Andrew Reynolds 2024-12-04 14:45:54 -06:00
  • 4130fefc04 Refactoring set defaults for safe options, full strict proofs (#11407) Andrew Reynolds 2024-12-04 13:15:48 -06:00
  • 9abbc68300 sygus: Refactor to not use NodeManager::currentNM() (#11394) Daniel Larraz 2024-12-04 12:28:37 -06:00
  • 50d193d5c7 Disable cpc on regression (#11405) Andrew Reynolds 2024-12-03 20:35:11 -06:00
  • 19a0ac9ae0 Add proper interface for skolem information in Node (#11404) Andrew Reynolds 2024-12-03 19:08:33 -06:00
  • bb3cb33324 Make several methods in NodeManager static (#11403) Andrew Reynolds 2024-12-03 17:45:25 -06:00
  • 9dfecba6b3 Add generic macro for rewriting body of quantified formulas (#11391) Andrew Reynolds 2024-12-03 17:25:14 -06:00
  • 4b1a47f309 Make QUANT_MERGE_PRENEX not eliminate duplicate variables, update QUANT_UNUSED_VARS (#11400) Andrew Reynolds 2024-12-03 15:12:59 -06:00
  • daab1239b5 Add infrastructure for proofs for witness terms (#11364) Andrew Reynolds 2024-12-03 11:32:35 -06:00
  • 9db602a5c9 Fix some typos in the documentation of two proof rules (#11384) Lachnitt 2024-12-03 08:00:09 -08:00
  • 37eea85583 Minor simplifications to theory interfaces (#11375) Andrew Reynolds 2024-12-02 15:41:49 -06:00
  • 3ba2c386f9 Never assign values to evaluable equivalence classes (#11322) Andrew Reynolds 2024-12-02 15:41:26 -06:00
  • d8b6d1c33f Create self-contained JARs for cvc5 Java bindings (#11368) Daniel Larraz 2024-12-02 12:53:01 -06:00
  • 6ff3d05708 Alethe: add name of trust rule as argument to alethe hole rules (#11398) Lachnitt 2024-12-02 04:27:16 -08:00
  • 8514715cbc Add proof logger interface (#11243) Andrew Reynolds 2024-11-26 15:56:26 -06:00
  • c5cb546711 Change ARITH_POLY_NORM_REL to avoid mixed arithmetic (#11387) Andrew Reynolds 2024-11-26 15:38:48 -06:00
  • df7773adb8 Add NodeManager pointer to NodeValue (#11320) Daniel Larraz 2024-11-26 09:12:26 -06:00
  • b8c109873a Fix lexer for symbols starting with ! (#11341) Andrew Reynolds 2024-11-23 15:46:52 -06:00
  • 0fddeedc0c Add two datatypes rules to CPC Eunoia signature (#11358) Andrew Reynolds 2024-11-22 16:52:15 -06:00
  • 3653506b2f Do not use cegqi-bv for quantifiers from quantifier elimination (#11344) Andrew Reynolds 2024-11-22 16:42:29 -06:00
  • 56f4230567 Add more cases of STRING_REDUCE in Eunoia (#11360) Andrew Reynolds 2024-11-22 16:23:13 -06:00
  • 665292e437 Add more cases for EVALUATE in Eunoia (#11359) Andrew Reynolds 2024-11-22 16:15:32 -06:00
  • bace760b6a Make preregister-mode a regular option (#11383) Andrew Reynolds 2024-11-22 14:30:56 -06:00
  • 7fc37ae58f Clarifying documentation for interpolation (#11380) yoni206 2024-11-21 22:40:00 +02:00
  • 4804b9c349 Handle cases of variable reordering in alpha equivalence proofs (#11381) Andrew Reynolds 2024-11-21 10:25:09 -06:00
  • 024c9822d7 Formalize more quantifiers theory rewrites in Eunoia (#11361) Andrew Reynolds 2024-11-21 08:13:15 -06:00
  • c645d256b8 Support bitvectors in Eunoia definition of ARITH_POLY_NORM (#11347) Andrew Reynolds 2024-11-20 21:53:17 -06:00
  • 41d49f91ef Make existing quant miniscope a macro, elaborate to simpler version (#11378) Andrew Reynolds 2024-11-20 18:55:00 -06:00
  • 0afac52956 Add three new BV RARE rules for handling TheoryBv::ppAssert (#11374) Andrew Reynolds 2024-11-20 18:34:25 -06:00
  • cb531649b6 Refactor RARE arithmetic rules to avoid mixed arithmetic (#11376) Andrew Reynolds 2024-11-20 18:34:05 -06:00
  • c1c590d35b Refactor static variables (#11379) Amalee Wilson 2024-11-20 13:03:51 -08:00
  • 35aaf57de8 Make quantifiers dynamic split proof producing (#11293) Andrew Reynolds 2024-11-20 11:24:06 -06:00
  • 08c0639030 Add licensing info for gcc-libs and winpthreads (#11365) Daniel Larraz 2024-11-19 15:30:32 -06:00
  • 5af5df511f Fix multithreading bugs (#11350) Amalee Wilson 2024-11-19 11:29:41 -08:00
  • b1c1d3bcc9 Track more fine grained trust ids in preprocessor (#11363) Andrew Reynolds 2024-11-19 11:28:03 -06:00
  • c462371fb2 Make ExtTheory proof producing (#11277) Andrew Reynolds 2024-11-19 10:06:40 -06:00
  • 449e9af043 Add ProofRewriteRule::DT_CYCLE (#11373) Andrew Reynolds 2024-11-19 10:05:39 -06:00
  • e1683d0874 Fix issue #11354 (#11372) mudathirmahgoub 2024-11-18 15:17:04 -06:00
  • ef0dc50ff9 Add proof support for missing datatypes inferences (#11304) Andrew Reynolds 2024-11-16 08:48:16 -06:00
  • 267ff8ecdd Make interface for ppStaticLearn able to track proofs (#11311) Andrew Reynolds 2024-11-15 15:10:59 -06:00
  • d1d842cff5 Fill in remaining datatypes rewrites (#11346) Andrew Reynolds 2024-11-15 15:10:37 -06:00
  • c12ed2dfeb Add trust id for arithmetic DIO lemmas (#11367) Andrew Reynolds 2024-11-15 13:05:25 -06:00
  • 27f6edd472 ci: Only install ethos and carcara when testing proofs (#11343) Daniel Larraz 2024-11-15 12:52:49 -06:00
  • a1637c8a56 Minor updates to BV RARE rules (#11345) Andrew Reynolds 2024-11-15 12:32:24 -06:00
  • 870cef591f Fix proof checking for ProofRule::CONCAT_CONFLICT_DEQ (#11370) Andrew Reynolds 2024-11-15 08:29:06 -06:00
  • 3336be60a8 Add extensionality rule ProofRule::STRINGS_EXT for sequences and strings (#11369) Andrew Reynolds 2024-11-15 08:28:33 -06:00
  • fcc54f0a1b Use ALPHA_EQUIV as a reconstruction tactic prior to RARE (#11330) Andrew Reynolds 2024-11-14 10:35:12 -06:00
  • e81f508eae Fix getInterpolant when top-level substitutions are present (#11340) Andrew Reynolds 2024-11-11 15:42:40 -06:00
  • a7021cd93a Add proof reconstruction for ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ (#11323) Andrew Reynolds 2024-11-09 09:14:22 -06:00
  • 44b240533a Add a few more missing proofs for sets interences (#11349) Andrew Reynolds 2024-11-09 09:14:09 -06:00
  • 77c64f33b9 [CPC] Ensure minus is used in contexts where it can be typed (#11333) Andrew Reynolds 2024-11-08 11:20:52 -06:00
  • 3db8490b5c Add Eunoia definition for ProofRule::ARITH_MULT_TANGENT (#11313) Andrew Reynolds 2024-11-07 09:53:30 -06:00
  • 23fd6166b4 Support ProofRule::ARITH_POLY_NORM_REL for bitvectors in Eunoia (#11314) Andrew Reynolds 2024-11-07 08:46:07 -06:00
  • 91e4ddf8e1 Add Eunoia definitions for missing quantifiers rules (#11305) Andrew Reynolds 2024-11-07 08:32:54 -06:00
  • a3f0848ab2 Minor fix in java docs. (#11342) Aina Niemetz 2024-11-06 11:33:16 -08:00
  • 6ba9aa3561 Refactoring naming scheme related to experimental theories, include FP (#11337) Andrew Reynolds 2024-11-06 11:43:27 -06:00
  • 545482a124 Use PRI macros to fix warnings in QuickStart C example (#11338) Daniel Larraz 2024-11-06 11:09:52 -06:00
  • cf2eeefc12 docs: Improve docs for getInterpolant. (#11339) Aina Niemetz 2024-11-06 06:13:37 -08:00
  • 40726ce3f4 Add RARE rewrites for arith bv conversions (#11336) Andrew Reynolds 2024-11-06 08:13:06 -06:00
  • 5288d22a73 More RARE string rewrites (#11335) Andrew Reynolds 2024-11-05 14:45:03 -06:00
  • 9779842ac8 Fixes and changes to BV overflow elimination rules (#11316) Andrew Reynolds 2024-11-05 13:40:27 -06:00
  • 99c6826950 Add a few more simple missing RARE rules (#11318) Andrew Reynolds 2024-11-05 13:37:02 -06:00
  • 86be9c0a66 Add a few more proofs for theory rewrites (#11284) Andrew Reynolds 2024-11-05 11:01:25 -06:00
  • 67517cbb84 Add proof support for several simple elimination theory rewrites (#11303) Andrew Reynolds 2024-11-04 08:59:41 -06:00