Code

Finite Field support#513

Code

Merged

ahmed-irfan merged 162 commits intoSRI-CSL:masterSRI-CSL/yices2:masterfrom Ovascos:ffsatOvascos/yices2:ffsatCopy head branch name to clipboardJul 3, 2024

+8,971-2,497

Commits

Commits on Nov 20, 2023

• Symbols created, eval_ff_* to be done

  

  Thomas Hader

  committed
  8c41f5f

  Copy full SHA for 8c41f5f

Commits on Nov 21, 2023

• Added ff_plugin stub

  

  Thomas Hader

  committed
  d8aab36

  Copy full SHA for d8aab36

• Registered ff plugin to mcsat

  

  Thomas Hader

  committed
  383e87d

  Copy full SHA for 383e87d

• Added further type support for FF type

  

  Thomas Hader

  committed
  d8eea38

  Copy full SHA for d8eea38

• Added printing support for the ff type

  

  Thomas Hader

  committed
  b257789

  Copy full SHA for b257789

• fixed warning

  

  Thomas Hader

  committed
  c1cb009

  Copy full SHA for c1cb009

Commits on Nov 22, 2023

• actual missing error strings

  

  Thomas Hader

  committed
  aed17f3

  Copy full SHA for aed17f3

Commits on Nov 23, 2023

• Parsing of (as (_ ff3 13) FF0) done

  

  Thomas Hader

  committed
  17b8ef6

  Copy full SHA for 17b8ef6

Commits on Nov 28, 2023

• reformat indentions

  

  Thomas Hader

  committed
  aecf376

  Copy full SHA for aecf376

Commits on Nov 29, 2023

• reformat indentions

  

  Thomas Hader

  committed
  3a4932d

  Copy full SHA for 3a4932d

• Front-end parsing done

  

  Thomas Hader

  committed
  283aa8b

  Copy full SHA for 283aa8b

Commits on Nov 30, 2023

• mod_rba_buffer_t and TAG_ARITH_FF_BUFFER

  

  Thomas Hader

  committed
  2035c47

  Copy full SHA for 2035c47

Commits on Dec 1, 2023

• Code Formatting

  

  Thomas Hader

  committed
  a10d403

  Copy full SHA for a10d403

Commits on Dec 2, 2023

• Finite Field term generation done

  

  Thomas Hader

  committed
  7a4ef2d

  Copy full SHA for 7a4ef2d

Commits on Dec 4, 2023

• Fixed print_elem in term_stack2.c

  

  Thomas Hader

  committed
  cf60337

  Copy full SHA for cf60337

Commits on Dec 5, 2023

• Code Formatting

  

  Thomas Hader

  committed
  65a9c3a

  Copy full SHA for 65a9c3a

• Removed unnecessary todos

  

  Thomas Hader

  committed
  211d1f1

  Copy full SHA for 211d1f1

• Support arbitrary finite field size

  

  Thomas Hader

  committed
  9a03d90

  Copy full SHA for 9a03d90

• Some optimization for ff eq term generation

  

  Thomas Hader

  committed
  36e83f9

  Copy full SHA for 36e83f9

Commits on Dec 6, 2023

• Code Formatting and Warning fixes

  

  Thomas Hader

  committed
  ba8887f

  Copy full SHA for ba8887f

• Added exceptions when ff is solved with non-mcsat context.

  

  Thomas Hader

  committed
  ae3399b

  Copy full SHA for ae3399b

• fixed model_eval to handle finite field terms (and return unknown).

  

  Thomas Hader

  committed
  46d8907

  Copy full SHA for 46d8907

• Term manager update (added further ff code to term_manager)

  

  Thomas Hader

  committed
  b4387c8

  Copy full SHA for b4387c8

• Added FF support to MCSAT preprocessor

  

  Thomas Hader

  committed
  085b9be

  Copy full SHA for 085b9be

• Added FF support to model printing

  

  Thomas Hader

  committed
  816b525

  Copy full SHA for 816b525

Commits on Dec 7, 2023

• fix

  

  Thomas Hader

  committed
  e849bd2

  Copy full SHA for e849bd2

• Fixed printing and added value_ff_t.

  

  Thomas Hader

  committed
  92f8e37

  Copy full SHA for 92f8e37

Commits on Dec 8, 2023

• WIP: ff_plugin_new_term_notify

  

  Thomas Hader

  committed
  088783e

  Copy full SHA for 088783e

• Code Formatting fixes

  

  Thomas Hader

  committed
  35afa14

  Copy full SHA for 35afa14

Commits on Dec 11, 2023

• extracted lp_data handling from NRA plugin

  

  Thomas Hader

  committed
  c93e4bd

  Copy full SHA for c93e4bd

• moved trail_variable_compare to trail and added lp_data in ff_plugin

  

  Thomas Hader

  committed
  16cc9b1

  Copy full SHA for 16cc9b1

Commits on Dec 12, 2023

• extracted poly_constraint from nra to lp_constraint_db

  

  Thomas Hader

  committed
  ecb37b0

  Copy full SHA for ecb37b0

• fixed bug in non mcsat part

  

  Thomas Hader

  committed
  92d6d54

  Copy full SHA for 92d6d54

Commits on Dec 13, 2023

• using lp_data in explanation

  

  Thomas Hader

  committed
  b66a2ec

  Copy full SHA for b66a2ec

• store term_t in lp_data instead of variable_t

  

  Thomas Hader

  committed
  aaaf162

  Copy full SHA for aaaf162

• Consolidated libpoly_utils.c

  

  Thomas Hader

  committed
  e63c2cc

  Copy full SHA for e63c2cc

Commits on Dec 14, 2023

• update nra_plugin_explain to support lp_data

  

  Thomas Hader

  committed
  348fefc

  Copy full SHA for 348fefc

Commits on Dec 15, 2023

• fixed context_config bug

  

  Thomas Hader

  committed
  f9636cc

  Copy full SHA for f9636cc

• added mcsat only checks to makefile

  

  Thomas Hader

  committed
  a4d8fab

  Copy full SHA for a4d8fab

• rework done: extracted lib_poly code from nra.

  

  Thomas Hader

  committed
  1cc4a46

  Copy full SHA for 1cc4a46

• rework done: extracted unit_info from nra and bv

  

  Thomas Hader

  committed
  35d4b90

  Copy full SHA for 35d4b90

• implementation of term_notify in ff done

  

  Thomas Hader

  committed
  e263fc0

  Copy full SHA for e263fc0

• fixed Makefile whitespaces

  

  Thomas Hader

  committed
  984c2a1

  Copy full SHA for 984c2a1

• ff_poly_constraint_create implemented and minor improvements in the nra plugin.

  

  Thomas Hader

  committed
  f4634de

  Copy full SHA for f4634de

Commits on Dec 19, 2023

• Build system update to use static libpoly for all builds when configured

  

  Thomas Hader

  committed
  ca54e9b

  Copy full SHA for ca54e9b

• fixed term printing issue

  

  Thomas Hader

  committed
  2652dfd

  Copy full SHA for 2652dfd

Commits on Jan 17, 2024

• make lp_data_t finite field order aware

  

  Thomas Hader

  committed
  b56a9e5

  Copy full SHA for b56a9e5

• throw exception on multiple ff orders

  

  Thomas Hader

  committed
  de85b45

  Copy full SHA for de85b45

• extracted constraint_unit_info_demote

  

  Thomas Hader

  committed
  da27533

  Copy full SHA for da27533

• Fixed typos

  

  Thomas Hader

  committed
  5884c47

  Copy full SHA for 5884c47

Commits on Jan 18, 2024

• minor code rework to enable the compiler to remove nra_plugin_check_assignment for release builds

  

  Thomas Hader

  committed
  3834ef3

  Copy full SHA for 3834ef3

• implemented pop/push and parts of propagate

  

  Thomas Hader

  committed
  2822709

  Copy full SHA for 2822709

• Typos and minor code fixes

  

  Thomas Hader

  committed
  b0a7bc5

  Copy full SHA for b0a7bc5

• Added feasible_int_set_db files

  

  Thomas Hader

  committed
  79ad351

  Copy full SHA for 79ad351

Commits on Jan 22, 2024

• value_version_set done

  

  Thomas Hader

  committed
  3a66453

  Copy full SHA for 3a66453

• Renamed to ff_feasible_set_db

  

  Thomas Hader

  committed
  6989c20

  Copy full SHA for 6989c20

• Attach/Detach lp_int_ring_t in ff_feasible_set

  

  Thomas Hader

  committed
  8c94793

  Copy full SHA for 8c94793

• added ff_feasible_set_db to ff_plugin

  

  Thomas Hader

  committed
  482a4b3

  Copy full SHA for 482a4b3

Commits on Jan 23, 2024

• Typos and minor code fixes

  

  Thomas Hader

  committed
  3d100ea

  Copy full SHA for 3d100ea

• ffsat propagation done

  

  Thomas Hader

  committed
  54d2e9b

  Copy full SHA for 54d2e9b

• fixed two assertions

  

  Thomas Hader

  committed
  9aa2cea

  Copy full SHA for 9aa2cea

• value_hash_map made first and next record operate on const value.

  

  Thomas Hader

  committed
  fd2eceb

  Copy full SHA for fd2eceb

• value_version_set fixed bugs

  

  Thomas Hader

  committed
  9cdb119

  Copy full SHA for 9cdb119

• Implemented ff_plugin_decide and some minor fixes

  

  Thomas Hader

  committed
  2fc4168

  Copy full SHA for 2fc4168

• Added calls to ff_feasible_set_db_pop/_push

  

  Thomas Hader

  committed
  927bed7

  Copy full SHA for 927bed7

Commits on Jan 24, 2024

• Using new libpoly features

  

  Thomas Hader

  committed
  4bcac43

  Copy full SHA for 4bcac43

• Fixed zero finding and some printing issues

  

  Thomas Hader

  committed
  a92ce4f

  Copy full SHA for a92ce4f

Commits on Jan 25, 2024

• Typos and minor code fixes

  

  Thomas Hader

  committed
  67e1eaa

  Copy full SHA for 67e1eaa

• Implemented ff_plugin_explain_propagation and ff_plugin_explain_evaluation (taken from nra)

  

  Thomas Hader

  committed
  4e00cbe

  Copy full SHA for 4e00cbe

• Created functions for ff explain

  

  Thomas Hader

  committed
  dc24552

  Copy full SHA for dc24552

• Typos and minor code fixes

  

  Thomas Hader

  committed
  3009617

  Copy full SHA for 3009617

• Prepared to plug explanation in

  

  Thomas Hader

  committed
  34c2b41

  Copy full SHA for 34c2b41

• Added explanation procedure

  

  Thomas Hader

  committed
  34348b5

  Copy full SHA for 34348b5

Commits on Jan 26, 2024

• Update ff_plugin_explain.c to avoid polynomial copying.

  

  Thomas Hader

  committed
  064d291

  Copy full SHA for 064d291

• Added plugin_ctx to lp_data

  

  Thomas Hader

  committed
  4b6f177

  Copy full SHA for 4b6f177

• fixed trace printing in ff_plugin_explain

  

  Thomas Hader

  committed
  e930613

  Copy full SHA for e930613

• Fixed some stuff

  

  Thomas Hader

  committed
  a69a38b

  Copy full SHA for a69a38b

Commits on Jan 28, 2024

• Fixed bugs in testing

  

  Thomas Hader

  committed
  dce78c0

  Copy full SHA for dce78c0

Commits on Jan 30, 2024

• Moved some code, addes some asserts

  

  Thomas Hader

  committed
  cec9f44

  Copy full SHA for cec9f44

• Some optimizations

  

  Thomas Hader

  committed
  882f3d0

  Copy full SHA for 882f3d0

• fixup

  

  Thomas Hader

  committed
  6852cfe

  Copy full SHA for 6852cfe

Commits on Jan 31, 2024

• fixed some bugs

  

  Thomas Hader

  committed
  62565b6

  Copy full SHA for 62565b6

• added last_reason_unsat conflict core minimization

  

  Thomas Hader

  committed
  be48c3a

  Copy full SHA for be48c3a

Commits on Feb 1, 2024

• added gc sweep in lp_data.c

  

  Thomas Hader

  committed
  02ead6c

  Copy full SHA for 02ead6c

• added irreducible factor calculation to ff_plugin_explain.c

  

  Thomas Hader

  committed
  aea2a94

  Copy full SHA for aea2a94

Commits on Feb 2, 2024

• added common factor removal

  

  Thomas Hader

  committed
  3ea2a09

  Copy full SHA for 3ea2a09

Commits on Feb 4, 2024

• added :dump-model option

  

  Thomas Hader

  committed
  9e90c2a

  Copy full SHA for 9e90c2a

• fixed ff model printing

  

  Thomas Hader

  committed
  bf2a43b

  Copy full SHA for bf2a43b

• Typos and minor code fixes

  

  Thomas Hader

  committed
  d0afd14

  Copy full SHA for d0afd14

• allowed ff-1

  

  Thomas Hader

  committed
  0629069

  Copy full SHA for 0629069

• Merge branch 'master' into ffsat

  

  Thomas Hader

  committed
  a4f01ee

  Copy full SHA for a4f01ee

Commits on Feb 7, 2024

• added todos/comments/ideas

  

  Thomas Hader

  committed
  12ada59

  Copy full SHA for 12ada59

• Fixed warnings in release build

  

  Thomas Hader

  committed
  668193b

  Copy full SHA for 668193b

Commits on Feb 9, 2024

• added libpoly root finding

  

  Thomas Hader

  committed
  d6f94b4

  Copy full SHA for d6f94b4

Commits on Feb 10, 2024

• fixed duplicated function

  

  Thomas Hader

  committed
  4371fe1

  Copy full SHA for 4371fe1

• fixed missing case in mcsat solver.c

  

  Thomas Hader

  committed
  8f5688e

  Copy full SHA for 8f5688e

• code format

  

  Thomas Hader

  committed
  b3b1d3e

  Copy full SHA for b3b1d3e

• Fixed todos in explain

  

  Thomas Hader

  committed
  db5dfe8

  Copy full SHA for db5dfe8

Commits on Feb 11, 2024

• added debugging code

  

  Thomas Hader

  committed
  e76b7f3

  Copy full SHA for e76b7f3

• report out of memory if rb and lp don't agree

  

  Thomas Hader

  committed
  d54e6cf

  Copy full SHA for d54e6cf

• Update Readme with special build steps

  

  Thomas Hader

  committed
  48682f3

  Copy full SHA for 48682f3

• Update readme

  

  Thomas Hader

  committed
  e4f1f1a

  Copy full SHA for e4f1f1a

• Update readme

  

  Thomas Hader

  committed
  1e57cad

  Copy full SHA for 1e57cad

Commits on Feb 12, 2024

• Fixed compile warnings

  

  Thomas Hader

  committed
  af688f9

  Copy full SHA for af688f9

Commits on Feb 13, 2024

• Fixed compile warnings in release build.

  

  Thomas Hader

  committed
  18fa128

  Copy full SHA for 18fa128

Commits on Feb 22, 2024

• Fixed typos

  

  Thomas Hader

  committed
  93d223d

  Copy full SHA for 93d223d

• rename int_queue_t size with capacity

  

  Thomas Hader

  committed
  b9ee6e1

  Copy full SHA for b9ee6e1

• enhanced int_queue

  

  Thomas Hader

  committed
  472deca

  Copy full SHA for 472deca

• added queue for next decision

  

  Thomas Hader

  committed
  ef12e80

  Copy full SHA for ef12e80

• Clear hint queue on conflict

  

  Thomas Hader

  committed
  d786129

  Copy full SHA for d786129

• Added two queues (top and hint)

  

  Thomas Hader

  committed
  5de62d2

  Copy full SHA for 5de62d2

• fixed bug

  

  Thomas Hader

  committed
  83bfa01

  Copy full SHA for 83bfa01

• added solver hints in NRA

  

  Thomas Hader

  committed
  6262396

  Copy full SHA for 6262396

• model_interpolation questions

  

  Thomas Hader

  committed
  36df734

  Copy full SHA for 36df734

• model_interpolation does not perform request_top_decision

  

  Thomas Hader

  committed
  8c32738

  Copy full SHA for 8c32738

• Remove shortcut variables from the queue

  

  Thomas Hader

  committed
  da32bd4

  Copy full SHA for da32bd4

• regression prints execution time

  

  Thomas Hader

  committed
  aec6c21

  Copy full SHA for aec6c21

• nra_plugin.c hint only on real solution

  

  Thomas Hader

  committed
  c0b0036

  Copy full SHA for c0b0036

• variable selection forces decision on hint

  

  Thomas Hader

  committed
  c429759

  Copy full SHA for c429759

• fix random decision

  

  Thomas Hader

  committed
  7fcca51

  Copy full SHA for 7fcca51

Commits on Feb 23, 2024

• trace printing

  

  Thomas Hader

  committed
  20deb56

  Copy full SHA for 20deb56

• changed the gold of a model interpolant

  

  Thomas Hader

  committed
  f4f6e58

  Copy full SHA for f4f6e58

Commits on Feb 26, 2024

• added option for test issue204.smt2

  

  Thomas Hader

  committed
  fdced2c

  Copy full SHA for fdced2c

Commits on Feb 28, 2024

• Merge branch 'decision-hint-queue' into ffsat-prop

  

  Thomas Hader

  committed
  81d1697

  Copy full SHA for 81d1697

Commits on Feb 29, 2024

• Added ff regression tests

  

  Thomas Hader

  committed
  8e4e98b

  Copy full SHA for 8e4e98b

• Added hint queue in ff

  

  Thomas Hader

  committed
  ace68f5

  Copy full SHA for ace68f5

Commits on Mar 2, 2024

• Added fintie field cases in substitution.c

  

  Thomas Hader

  committed
  ce43ad3

  Copy full SHA for ce43ad3

• Added const to rational functions

  

  Thomas Hader

  committed
  bfb7c4b

  Copy full SHA for bfb7c4b

• Made ff order (rational_t *mod) const

  

  Thomas Hader

  committed
  f10ecd9

  Copy full SHA for f10ecd9

• Some code rework and fixed missing mod calculation in arith_ff_buffer_to_term

  

  Thomas Hader

  committed
  dbd7e5f

  Copy full SHA for dbd7e5f

Commits on Mar 8, 2024

• renamed srs to lp_polynomial_subres in libpoly

  

  Thomas Hader

  committed
  87eb50d

  Copy full SHA for 87eb50d

• Merge branch 'master' into ffsat

  

  Thomas Hader

  committed
  f4506d2

  Copy full SHA for f4506d2

• removed changes to build system (align with master)

  

  Thomas Hader

  committed
  e67c3bb

  Copy full SHA for e67c3bb

Commits on Mar 9, 2024

• minor reworks in feasible_set_db and nra_plugin

  

  Thomas Hader

  committed
  9ac1cb9

  Copy full SHA for 9ac1cb9

• Integrated lp_feasibility_set_int in ff_plugin

  

  Thomas Hader

  committed
  a197571

  Copy full SHA for a197571

Commits on Mar 11, 2024

• Added quickxplain to ff_feasible_set_db

  

  Thomas Hader

  committed
  1c031dc

  Copy full SHA for 1c031dc

• Added pointer to nra_plugin in feasible_set_db

  

  Thomas Hader

  committed
  50b7543

  Copy full SHA for 50b7543

Commits on May 23, 2024

• Merge branch 'master' into ffsat

  

  Thomas Hader

  committed
  dfd99e1

  Copy full SHA for dfd99e1

• Changed the finite field logic from FF to FFA

  

  Thomas Hader

  committed
  9e52562

  Copy full SHA for 9e52562

Commits on May 24, 2024

• Code Formatting fixes

  

  Thomas Hader

  committed
  967f979

  Copy full SHA for 967f979

• Minor code cleanup

  

  Thomas Hader

  committed
  ee37100

  Copy full SHA for ee37100

• Added comment

  

  Thomas Hader

  committed
  d644070

  Copy full SHA for d644070

• Reverted README.md

  

  Thomas Hader

  committed
  bf39b5d

  Copy full SHA for bf39b5d

• Merge branch 'ffsat-prop' into ffsat

  

  Thomas Hader

  committed
  fc2bcc0

  Copy full SHA for fc2bcc0

• Removed broken runtime estimate from check.sh

  

  Thomas Hader

  committed
  7f54071

  Copy full SHA for 7f54071

• added more const

  

  Thomas Hader

  committed
  d87ddf6

  Copy full SHA for d87ddf6

• Fixed false-positive warning in gcc

  

  Thomas Hader

  committed
  da66d3d

  Copy full SHA for da66d3d

Commits on May 29, 2024

• Merge branch 'ccm' into ffsat

  

  Thomas Hader

  committed
  83baf76

  Copy full SHA for 83baf76

• Removed non-passing test

  

  Thomas Hader

  committed
  76e0a5d

  Copy full SHA for 76e0a5d

Commits on Jun 20, 2024

• Merge branch 'master' into ffsat

  

  Thomas Hader

  committed
  853ba28

  Copy full SHA for 853ba28

• Removed additional check code, since issue 520 is fixed

  

  Thomas Hader

  committed
  97b6c2e

  Copy full SHA for 97b6c2e

Commits on Jun 25, 2024

• Fixed typos

  

  Thomas Hader

  committed
  bf87888

  Copy full SHA for bf87888

• Added missing FFA in arith framgemt_names

  

  Thomas Hader

  committed
  ab931a6

  Copy full SHA for ab931a6

• Merge branch 'master' into ffsat

  Ovascos

  authored
  c22826a

  Copy full SHA for c22826a

• run_test.sh: removed tailing } in filenames

  

  Thomas Hader

  committed
  a9cbc58

  Copy full SHA for a9cbc58

Commits on Jun 26, 2024

• Adaptions to feedback, part 1

  

  Thomas Hader

  committed
  6878c3d

  Copy full SHA for 6878c3d

Commits on Jun 28, 2024

• Minor rework

  

  Thomas Hader

  committed
  5f680ad

  Copy full SHA for 5f680ad

Commits on Jul 1, 2024

• Adaptions to feedback, part 2

  

  Thomas Hader

  committed
  cb7ba67

  Copy full SHA for cb7ba67

• Removed unused value_version_set

  

  Thomas Hader

  committed
  79e60b6

  Copy full SHA for 79e60b6

Commits on Jul 2, 2024

• Updated FFA error printing

  

  Thomas Hader

  committed
  a362b79

  Copy full SHA for a362b79

• Update comments

  

  Thomas Hader

  committed
  df03f4f

  Copy full SHA for df03f4f

• fixed test gold file

  

  Thomas Hader

  committed
  c7ddc21

  Copy full SHA for c7ddc21