Code

MaxSMT solver implementation#137

Code

Draft

viktoriia-fomina wants to merge 243 commits intoUnitTestBot:mainUnitTestBot/ksmt:mainfrom viktoriia-fomina:maxsmtviktoriia-fomina/ksmt:maxsmtCopy head branch name to clipboard

+5,916-124

Commits

Commits on Jun 22, 2023

• Proto is in progress

  viktoriia-fomina

  committed
  0533a20

  Copy full SHA for 0533a20

Commits on Jun 23, 2023

• Simple cases work

  viktoriia-fomina

  committed
  561afed

  Copy full SHA for 561afed

• Refactor: getUnsatCoreOfConstraints, context

  viktoriia-fomina

  committed
  9d02516

  Copy full SHA for 9d02516

• Do not keep and remove from formula hard constraints

  viktoriia-fomina

  committed
  d8b4780

  Copy full SHA for d8b4780

• Split formula and soft constraints meaning

  viktoriia-fomina

  committed
  c6351cd

  Copy full SHA for c6351cd

Commits on Jun 26, 2023

• Improve wording in variable names

  viktoriia-fomina

  committed
  72d2f97

  Copy full SHA for 72d2f97

• Update methods' order

  viktoriia-fomina

  committed
  760d7d4

  Copy full SHA for 760d7d4

• Do not keep and remove from formula hard constraints

  viktoriia-fomina

  committed
  5ba890e

  Copy full SHA for 5ba890e

• Add smoke tests

  viktoriia-fomina

  committed
  2efbc5b

  Copy full SHA for 2efbc5b

• Merge main branch

  viktoriia-fomina

  committed
  657e0a3

  Copy full SHA for 657e0a3

• Fix bug with list subtraction im ApplyMaxRes, fix when styles, add more tests

  viktoriia-fomina

  committed
  00aa09a

  Copy full SHA for 00aa09a

Commits on Jun 27, 2023

• Support weighted soft constraints, soft constraints with duplicate expression , add more tests, rename to MaxSat

  viktoriia-fomina

  committed
  1ab1638

  Copy full SHA for 1ab1638

Commits on Jun 28, 2023

• Create MaxSATResult class, generalize KMaxSATSolver class

  viktoriia-fomina

  committed
  b44203b

  Copy full SHA for b44203b

• Improve tests, do unionSoftConstraintsWithSameExpressions when get formula,

  viktoriia-fomina

  committed
  88bc4af

  Copy full SHA for 88bc4af

• Remove TODO from tests, add docs to methods, update their names

  viktoriia-fomina

  committed
  cec69ed

  Copy full SHA for cec69ed

• Simplify expression in checkMaxSAT (removes TODO)

  viktoriia-fomina

  committed
  522c6a9

  Copy full SHA for 522c6a9

• Add more comments

  viktoriia-fomina

  committed
  7be0435

  Copy full SHA for 7be0435

• Do hard constraints work with push/pop

  viktoriia-fomina

  committed
  ffff397

  Copy full SHA for ffff397

Commits on Jun 29, 2023

• Support push/pop for soft constraints, use shorter expressions form in tests

  viktoriia-fomina

  committed
  14d8bdd

  Copy full SHA for 14d8bdd

Commits on Jun 30, 2023

• Optimize algorithm (remove added that is later removed), fix a bug in split unsat core (if the same expressions weight was equal, both of them were added to the core).

  viktoriia-fomina

  committed
  6b680c4

  Copy full SHA for 6b680c4

• Add inequalities test

  viktoriia-fomina

  committed
  3e9afec

  Copy full SHA for 3e9afec

• Rename soft constraint property: constraint -> expression

  viktoriia-fomina

  committed
  3a14625

  Copy full SHA for 3a14625

Commits on Jul 3, 2023

• Add timeout support, improve KMaxSATResult

  viktoriia-fomina

  committed
  e3c07f3

  Copy full SHA for e3c07f3

• Expression length growth: quadratic -> linear

  viktoriia-fomina

  committed
  ae12b77

  Copy full SHA for ae12b77

• Return accidently removed

  viktoriia-fomina

  committed
  68ba4ed

  Copy full SHA for 68ba4ed

• Update build.gradle.kts for max-sat module

  viktoriia-fomina

  committed
  c3ccb57

  Copy full SHA for c3ccb57

Commits on Jul 4, 2023

• applyMaxRes: add lost soft constraint, format code

  viktoriia-fomina

  committed
  b44279f

  Copy full SHA for b44279f

• Use with(ctx) in solver for more readable expressions

  viktoriia-fomina

  committed
  51739d6

  Copy full SHA for 51739d6

• Rewrite KOrNaryExpr through reduce

  viktoriia-fomina

  committed
  908175d

  Copy full SHA for 908175d

• Throw NotImplementedError when unsat and timeout exceeded

  viktoriia-fomina

  committed
  6aa4c50

  Copy full SHA for 6aa4c50

• Add comments to MaxSATScopeManager, remove redundant classes

  viktoriia-fomina

  committed
  9d68212

  Copy full SHA for 9d68212

• Comment KMaxSATResult, add default value to pop in MaxSATScopeManager

  viktoriia-fomina

  committed
  972a521

  Copy full SHA for 972a521

• Refactor: more Kotlin style in MaxSATSolver

  viktoriia-fomina

  committed
  da70d6e

  Copy full SHA for da70d6e

Commits on Jul 5, 2023

• Remove useless file: Main.kt

  viktoriia-fomina

  committed
  04d582d

  Copy full SHA for 04d582d

Commits on Jul 26, 2023

• Do weight unsigned, fix reification variables markers (bugfix)

  viktoriia-fomina

  committed
  c773870

  Copy full SHA for c773870

Commits on Jul 27, 2023

• Merge branch 'UnitTestBot:main' into max-sat

  viktoriia-fomina

  authored
  c709ca9

  Copy full SHA for c709ca9

• Merge branch 'max-sat' of https://github.com/victoriafomina/ksmt into max-sat

  viktoriia-fomina

  committed
  f19805e

  Copy full SHA for f19805e

Commits on Aug 4, 2023

• Add timeout

  viktoriia-fomina

  committed
  6b84643

  Copy full SHA for 6b84643

Commits on Aug 7, 2023

• Add ksmt-maxsat-tests project

  viktoriia-fomina

  committed
  6feb1e6

  Copy full SHA for 6feb1e6

• Merge branch 'main' into max-sat

  viktoriia-fomina

  authored
  0e44ae2

  Copy full SHA for 0e44ae2

• Ignore maxsat test data

  viktoriia-fomina

  committed
  52ab4e1

  Copy full SHA for 52ab4e1

• Update timeout value

  viktoriia-fomina

  committed
  05fb157

  Copy full SHA for 05fb157

Commits on Aug 8, 2023

• Run benchmark on single runner

  viktoriia-fomina

  committed
  472f367

  Copy full SHA for 472f367

• Fix bug with return type in SmtLibBenchmarkUtil

  viktoriia-fomina

  committed
  e3f1467

  Copy full SHA for e3f1467

Commits on Aug 9, 2023

• Move MaxRes algorithm to a separate solver

  viktoriia-fomina

  committed
  4642aff

  Copy full SHA for 4642aff

Commits on Aug 10, 2023

• Use minOf instead of minBy

  viktoriia-fomina

  committed
  7ed9360

  Copy full SHA for 7ed9360

Commits on Aug 30, 2023

• Implement primal dual MaxRes solver

  Show description for a01c1bb
  viktoriia-fomina

  committed
  a01c1bb

  Copy full SHA for a01c1bb

• Add timeout support for primal dual MaxRes solver

  viktoriia-fomina

  committed
  d4b5c39

  Copy full SHA for d4b5c39

Commits on Aug 31, 2023

• Add KMaxSatContext

  Show description for d4422bd
  viktoriia-fomina

  committed
  d4422bd

  Copy full SHA for d4422bd

• Fix tests: pass MaxSAT context to KPrimalDualMaxResSolver constructor

  viktoriia-fomina

  committed
  73af599

  Copy full SHA for 73af599

• Add hill-climb approach when checking satisfiability

  viktoriia-fomina

  committed
  f584b31

  Copy full SHA for f584b31

• Let extract a single core or multiple cores

  viktoriia-fomina

  committed
  7eb8b40

  Copy full SHA for 7eb8b40

Commits on Sep 8, 2023

• Fix a bug when getting a single core in KPrimalDualMaxResSolver

  viktoriia-fomina

  committed
  59e652a

  Copy full SHA for 59e652a

• Add unit tests for all configurations

  Show description for 43b6b69
  viktoriia-fomina

  committed
  43b6b69

  Copy full SHA for 43b6b69

Commits on Oct 5, 2023

• Support running MaxSMT benchmark tests

  viktoriia-fomina

  committed
  18fe5a2

  Copy full SHA for 18fe5a2

• Add similar expressions test

  viktoriia-fomina

  committed
  ce4a5fa

  Copy full SHA for ce4a5fa

Commits on Oct 6, 2023

• Merge branch 'UnitTestBot:main' into max-sat

  viktoriia-fomina

  authored
  931bde8

  Copy full SHA for 931bde8

Commits on Oct 19, 2023

• Set up running long MaxSMT tests

  viktoriia-fomina

  committed
  72d21fe

  Copy full SHA for 72d21fe

• Merge branch 'UnitTestBot:main' into max-sat

  viktoriia-fomina

  authored
  aaa6aa0

  Copy full SHA for aaa6aa0

• Rename MaxSATBenchmarkUtil to MaxSMTBenchmarkUtil

  viktoriia-fomina

  committed
  8df4622

  Copy full SHA for 8df4622

Commits on Oct 20, 2023

• Update test data directory

  viktoriia-fomina

  committed
  0c722ca

  Copy full SHA for 0c722ca

Commits on Oct 23, 2023

• Create monitoring.sh

  viktoriia-fomina

  authored
  8244dd8

  Copy full SHA for 8244dd8

• Add monitoring to long tests launch

  viktoriia-fomina

  authored
  8ce6098

  Copy full SHA for 8ce6098

• Add more MaxSMT unit tests

  viktoriia-fomina

  committed
  2999243

  Copy full SHA for 2999243

• Add messages to MaxSMT benchmark tests assertions

  viktoriia-fomina

  committed
  d39fb0c

  Copy full SHA for d39fb0c

• Update maxsmt-tests-matrix.json

  viktoriia-fomina

  authored
  26048aa

  Copy full SHA for 26048aa

• Update logics for MaxSMT tests

  viktoriia-fomina

  committed
  234ee20

  Copy full SHA for 234ee20

• Merge branch 'max-sat' of https://github.com/victoriafomina/ksmt into max-sat

  viktoriia-fomina

  committed
  b11a900

  Copy full SHA for b11a900

Commits on Oct 25, 2023

• Upgrade Kotlin version to 1.9.0

  viktoriia-fomina

  committed
  fa05d47

  Copy full SHA for fa05d47

• Rename maxsat subproject to maxsmt

  viktoriia-fomina

  committed
  895193d

  Copy full SHA for 895193d

• Merge branch 'UnitTestBot:main' into maxsmt

  viktoriia-fomina

  authored
  bdd471f

  Copy full SHA for bdd471f

Commits on Oct 26, 2023

• Update maxsmt-tests-matrix.json

  viktoriia-fomina

  authored
  4e116fb

  Copy full SHA for 4e116fb

• Update tests list in build.gradle.kts

  viktoriia-fomina

  committed
  51f2006

  Copy full SHA for 51f2006

• Merge branch 'maxsmt' of https://github.com/victoriafomina/ksmt into maxsmt

  viktoriia-fomina

  committed
  cf787e7

  Copy full SHA for cf787e7

• Rename maxsat project to maxsmt in workflows

  viktoriia-fomina

  committed
  efb04b8

  Copy full SHA for efb04b8

• Add QF_AUFLIA to MaxSMT tests

  viktoriia-fomina

  committed
  83a03e7

  Copy full SHA for 83a03e7

• Fix MaxSMT test assert message

  viktoriia-fomina

  committed
  abd32e2

  Copy full SHA for abd32e2

Commits on Oct 30, 2023

• Update build.gradle.kts

  viktoriia-fomina

  committed
  2215161

  Copy full SHA for 2215161

• Update maxsmt-tests-matrix.json

  viktoriia-fomina

  authored
  16abc14

  Copy full SHA for 16abc14

• Update run-long-maxsmt-tests.yml

  viktoriia-fomina

  authored
  9a35343

  Copy full SHA for 9a35343

• Create KPrimalDualMaxResSMTBenchmarkTest.kt

  viktoriia-fomina

  committed
  cbf8f6b

  Copy full SHA for cbf8f6b

• Merge branch 'maxsmt' of https://github.com/victoriafomina/ksmt into maxsmt

  viktoriia-fomina

  committed
  819d4c1

  Copy full SHA for 819d4c1

Commits on Nov 8, 2023

• Merge branch 'UnitTestBot:main' into maxsmt

  viktoriia-fomina

  authored
  ad03400

  Copy full SHA for ad03400

Commits on Nov 9, 2023

• Fix a bug in core minimization

  viktoriia-fomina

  committed
  b8eb117

  Copy full SHA for b8eb117

• Add asserts to similar expressions test

  viktoriia-fomina

  committed
  e6d2549

  Copy full SHA for e6d2549

Commits on Nov 10, 2023

• Add test when three expressions are inconsistent

  viktoriia-fomina

  committed
  684b371

  Copy full SHA for 684b371

• Fix typo in .gitignore

  viktoriia-fomina

  committed
  350a5c4

  Copy full SHA for 350a5c4

• Add possibility to choose solver for MaxSMT benchmark tests

  viktoriia-fomina

  committed
  e2a8f2a

  Copy full SHA for e2a8f2a

• Update run-long-maxsmt-tests.yml: support choosing solver

  viktoriia-fomina

  authored
  7643f6a

  Copy full SHA for 7643f6a

• Update run-long-maxsmt-tests.yml: update test report name

  viktoriia-fomina

  authored
  73451b4

  Copy full SHA for 73451b4

• Run PDMRes solver benchmark tests in different configurations

  viktoriia-fomina

  committed
  03ce90f

  Copy full SHA for 03ce90f

• Format KMaxSMTSolverTest.kt

  viktoriia-fomina

  committed
  6a33a56

  Copy full SHA for 6a33a56

Commits on Nov 16, 2023

• Add statistics collection

  viktoriia-fomina

  committed
  b12e8f4

  Copy full SHA for b12e8f4

Commits on Nov 17, 2023

• Add more test data

  viktoriia-fomina

  committed
  ad0c2c3

  Copy full SHA for ad0c2c3

Commits on Nov 20, 2023

• Refactor checking hard constraints in KPMResSolver

  viktoriia-fomina

  committed
  b3d52ff

  Copy full SHA for b3d52ff

• Update assertions in MaxSMT tests

  viktoriia-fomina

  committed
  3a57541

  Copy full SHA for 3a57541

Commits on Nov 23, 2023

• Fix KPrimalDualMaxRes solver bugs

  Show description for b1530da
  viktoriia-fomina

  committed
  b1530da

  Copy full SHA for b1530da

Commits on Nov 24, 2023

• Add more logics for MaxSMT tests

  viktoriia-fomina

  committed
  21d104d

  Copy full SHA for 21d104d

Commits on Nov 28, 2023

• Run solvers only on supported theories for MaxSMT tests

  viktoriia-fomina

  committed
  265fe5b

  Copy full SHA for 265fe5b

Commits on Nov 29, 2023

• Add QF_UF MaxSMT test data

  viktoriia-fomina

  committed
  670fa11

  Copy full SHA for 670fa11

• Generalize solvers configurations in tests using out

  viktoriia-fomina

  committed
  0232cac

  Copy full SHA for 0232cac

• Add QF_AUFBV MaxSMT test data

  viktoriia-fomina

  committed
  40b00f0

  Copy full SHA for 40b00f0

• Generalize solver in MaxSAT tests

  viktoriia-fomina

  committed
  a34677d

  Copy full SHA for a34677d

• Rename solver to Yices in workflow

  viktoriia-fomina

  committed
  27f106d

  Copy full SHA for 27f106d

Commits on Nov 30, 2023

• Update QF_ABVFP MaxSMT benchmark information

  viktoriia-fomina

  committed
  78d9073

  Copy full SHA for 78d9073

Commits on Dec 1, 2023

• Collect and merge MaxSMT test run statistics

  viktoriia-fomina

  committed
  69461f7

  Copy full SHA for 69461f7

• Add SMT solver name to statistics

  viktoriia-fomina

  committed
  ec71037

  Copy full SHA for ec71037

• Add QF_FP MaxSMT test data

  viktoriia-fomina

  committed
  5d042a4

  Copy full SHA for 5d042a4

• Add comments to MaxSMT benchmark workflow

  viktoriia-fomina

  committed
  3bab490

  Copy full SHA for 3bab490

• Update to always add logic name to statistics

  viktoriia-fomina

  committed
  4dbe40f

  Copy full SHA for 4dbe40f

• Move SAT soft constraints sum calculation in tests

  viktoriia-fomina

  committed
  52123c2

  Copy full SHA for 52123c2

• Collect statistics from ignored, failed when parsing file/convert expressions test

  viktoriia-fomina

  committed
  c4c0f75

  Copy full SHA for c4c0f75

• Merge branch 'UnitTestBot:main' into maxsmt

  viktoriia-fomina

  authored
  1912f64

  Copy full SHA for 1912f64

• Add QF_UFBV MaxSMT test data

  viktoriia-fomina

  committed
  1c3081c

  Copy full SHA for 1c3081c

• Remove elapsed time from MaxSMTTestStatistics

  Show description for 21f58ec
  viktoriia-fomina

  committed
  21f58ec

  Copy full SHA for 21f58ec

• Run MaxSMT tests on Ubuntu-20.04

  viktoriia-fomina

  committed
  9c856db

  Copy full SHA for 9c856db

• Add script analyzing statistics

  viktoriia-fomina

  committed
  b07a245

  Copy full SHA for b07a245

• Add statistics analysis to MaxSMT benchmark workflow

  viktoriia-fomina

  committed
  da3d854

  Copy full SHA for da3d854

• Move analyze MaxSMT test run statistics step

  viktoriia-fomina

  committed
  429eaa1

  Copy full SHA for 429eaa1

• Fix work with JSON in statistics analyzer

  viktoriia-fomina

  committed
  0940065

  Copy full SHA for 0940065

• Set up encoding in JSON analyzer

  viktoriia-fomina

  committed
  2a694bf

  Copy full SHA for 2a694bf

Commits on Dec 2, 2023

• Add repository checkout in MaxSMT benchmark workflow

  viktoriia-fomina

  committed
  9744336

  Copy full SHA for 9744336

Commits on Dec 3, 2023

• Generate statistics with random string suffix

  viktoriia-fomina

  committed
  0ddf3a1

  Copy full SHA for 0ddf3a1

• Fix a bug with core minimization

  viktoriia-fomina

  committed
  1ae2639

  Copy full SHA for 1ae2639

Commits on Dec 4, 2023

• Add lost path to MaxSMT statistics analyzer script

  viktoriia-fomina

  committed
  764a8c5

  Copy full SHA for 764a8c5

• Do core minimization optional for KPDMRes

  viktoriia-fomina

  committed
  bb3aa19

  Copy full SHA for bb3aa19

Commits on Dec 6, 2023

• Use == instead of internEquals

  viktoriia-fomina

  committed
  c5f6ab4

  Copy full SHA for c5f6ab4

• Divide MaxSMT tests by primal and dual strategies

  viktoriia-fomina

  committed
  e223e75

  Copy full SHA for e223e75

• Ignore MaxSMT statistics files

  viktoriia-fomina

  committed
  d4d660f

  Copy full SHA for d4d660f

• Divide MaxSMT workflows into PMRes and PrimalDualMaxRes

  viktoriia-fomina

  committed
  ce4dd73

  Copy full SHA for ce4dd73

• Do not union soft constraints with same expressions

  viktoriia-fomina

  committed
  655335a

  Copy full SHA for 655335a

Commits on Dec 7, 2023

• Fix checking out commit in the MaxSMT workflow

  viktoriia-fomina

  committed
  6b43cac

  Copy full SHA for 6b43cac

• Add QF_ABV MaxSMT test data

  viktoriia-fomina

  committed
  5f293d3

  Copy full SHA for 5f293d3

• Fix the bug with duplicated test statistics collection

  viktoriia-fomina

  committed
  d911a7b

  Copy full SHA for d911a7b

• Update MaxSMT tests archives sizes

  viktoriia-fomina

  committed
  9c12bd4

  Copy full SHA for 9c12bd4

• Expand analyzed MaxSMT statistics content

  viktoriia-fomina

  committed
  4c41c30

  Copy full SHA for 4c41c30

• Add QF_AUFLIA MaxSMT test data

  viktoriia-fomina

  committed
  dcddae4

  Copy full SHA for dcddae4

• Add QF_UFLIA MaxSMT test data

  viktoriia-fomina

  committed
  ef39f8c

  Copy full SHA for ef39f8c

Commits on Dec 8, 2023

• Update MaxSAT workflow in order to run tests on multiple runners

  viktoriia-fomina

  committed
  c6bb303

  Copy full SHA for c6bb303

Commits on Dec 11, 2023

• Process cases when exception is thrown during MaxSMT solving

  viktoriia-fomina

  committed
  52f0335

  Copy full SHA for 52f0335

Commits on Dec 12, 2023

• Update MaxSMT tests timeout

  viktoriia-fomina

  committed
  7f31dd4

  Copy full SHA for 7f31dd4

Commits on Jan 16, 2024

• Log events in KPrimalDualMaxResSolver

  viktoriia-fomina

  committed
  1c84b45

  Copy full SHA for 1c84b45

• Upload test logs in MaxSMT workflow

  viktoriia-fomina

  committed
  238f9bd

  Copy full SHA for 238f9bd

Commits on Jan 17, 2024

• Use ValueTimeMark for time measurement

  viktoriia-fomina

  committed
  dd3b16b

  Copy full SHA for dd3b16b

• Log more events

  viktoriia-fomina

  committed
  5c9144d

  Copy full SHA for 5c9144d

Commits on Jan 18, 2024

• Log unsucceeded MaxSMT execution

  viktoriia-fomina

  committed
  c33d2bd

  Copy full SHA for c33d2bd

• Update default value for KMaxSMTContext

  viktoriia-fomina

  committed
  211e2af

  Copy full SHA for 211e2af

• Update logs about models

  viktoriia-fomina

  committed
  6fdb930

  Copy full SHA for 6fdb930

Commits on Jan 19, 2024

• Fix hill climb option

  viktoriia-fomina

  committed
  adc89ad

  Copy full SHA for adc89ad

Commits on Jan 23, 2024

• Update getting disjoint unsat cores option

  viktoriia-fomina

  committed
  354affa

  Copy full SHA for 354affa

• Log lower bound updates

  viktoriia-fomina

  committed
  5d14b5a

  Copy full SHA for 5d14b5a

Commits on Jan 24, 2024

• Add NotYetImplementedException

  viktoriia-fomina

  committed
  ffea92d

  Copy full SHA for ffea92d

Commits on Jan 25, 2024

• Refactor KPMResSolver

  viktoriia-fomina

  committed
  0f161f4

  Copy full SHA for 0f161f4

• Fix a bug with a core to soft constraints transformation

  viktoriia-fomina

  committed
  fe3b272

  Copy full SHA for fe3b272

• Add GSON version to properties

  viktoriia-fomina

  committed
  d2a0f3e

  Copy full SHA for d2a0f3e

Commits on Mar 23, 2024

• Merge branch 'UnitTestBot:main' into maxsmt

  viktoriia-fomina

  authored
  49172ec

  Copy full SHA for 49172ec

Commits on Apr 17, 2024

• Merge branch 'main' into maxsmt

  viktoriia-fomina

  authored
  e94beaa

  Copy full SHA for e94beaa

Commits on Apr 28, 2024

• Merge branch 'main' into maxsmt

  viktoriia-fomina

  authored
  cc255d9

  Copy full SHA for cc255d9

• Add checkSubOptMaxSMT method to KPrimalDualMaxResSolver

  viktoriia-fomina

  committed
  f03b984

  Copy full SHA for f03b984

Commits on Apr 30, 2024

• Add test run for Portfolio

  viktoriia-fomina

  committed
  60ff5c3

  Copy full SHA for 60ff5c3

• Fix comment for MinimalUnsatCore

  viktoriia-fomina

  committed
  ae059fc

  Copy full SHA for ae059fc

• Add default params to checkSubOptMaxSMT

  viktoriia-fomina

  committed
  4aa0762

  Copy full SHA for 4aa0762

• Implement portfolio mode with MaxSMT logic in the backend process

  viktoriia-fomina

  committed
  448f1f0

  Copy full SHA for 448f1f0

Commits on May 2, 2024

• Update Portfolio using rd

  viktoriia-fomina

  committed
  0801086

  Copy full SHA for 0801086

• Transfer solverManager creation/closing to before/after All

  viktoriia-fomina

  committed
  64e17c9

  Copy full SHA for 64e17c9

• Add Portfolio solver to KMaxSMTBenchmarkTest

  viktoriia-fomina

  committed
  0937081

  Copy full SHA for 0937081

• Support portfolio for statistics on CI

  viktoriia-fomina

  committed
  2f4236e

  Copy full SHA for 2f4236e

• Fix path to configurations

  viktoriia-fomina

  committed
  14280b6

  Copy full SHA for 14280b6

• Pass optimality from PDMRes workflow

  viktoriia-fomina

  committed
  3610a0b

  Copy full SHA for 3610a0b

• Fix syntax error in workflow

  viktoriia-fomina

  committed
  abcd7d4

  Copy full SHA for abcd7d4

• Fix workflow error

  viktoriia-fomina

  committed
  55a3df0

  Copy full SHA for 55a3df0

• Update statistics path

  viktoriia-fomina

  committed
  b8757e4

  Copy full SHA for b8757e4

• Downgrade upload-action version in order to use wilcard path

  viktoriia-fomina

  committed
  0b87c8f

  Copy full SHA for 0b87c8f

• Upgrade upload-artifact version

  viktoriia-fomina

  committed
  97c2ace

  Copy full SHA for 97c2ace

• Upgrade Ubuntu version

  viktoriia-fomina

  committed
  ab8cb9d

  Copy full SHA for ab8cb9d

• Remove redundant lines

  viktoriia-fomina

  committed
  12e8723

  Copy full SHA for 12e8723

Commits on May 10, 2024

• Update SolverProtocolModel

  viktoriia-fomina

  committed
  fef02cd

  Copy full SHA for fef02cd

• Process UNKNOWN cases in KPMResSolver

  viktoriia-fomina

  committed
  af14e36

  Copy full SHA for af14e36

• Add debug step to workflow

  viktoriia-fomina

  committed
  b114218

  Copy full SHA for b114218

• Upgrade download action version

  viktoriia-fomina

  committed
  1697ec0

  Copy full SHA for 1697ec0

• Remove debug step in workflow

  viktoriia-fomina

  committed
  b1d0979

  Copy full SHA for b1d0979

• Collect statistics about all theories

  viktoriia-fomina

  committed
  6be8ce9

  Copy full SHA for 6be8ce9

• Fix a bug with optimalWeight in KSubOptMaxSMTBenchmarkTest

  viktoriia-fomina

  committed
  506ba0c

  Copy full SHA for 506ba0c

• Fix a bug with score collection

  viktoriia-fomina

  committed
  cb5d1b4

  Copy full SHA for cb5d1b4

Commits on May 11, 2024

• Use solverQuery for checkMaxSMT in KPortfolioSolver

  viktoriia-fomina

  committed
  b3053c3

  Copy full SHA for b3053c3

• Update workers number

  viktoriia-fomina

  committed
  c0241a0

  Copy full SHA for c0241a0

Commits on May 12, 2024

• Fix a bug with internalizing assertions for Portfolio

  viktoriia-fomina

  committed
  7bec874

  Copy full SHA for 7bec874

• Update timeout to 10 seconds

  viktoriia-fomina

  committed
  53c303c

  Copy full SHA for 53c303c

• Update timeout for MaxSAT tests

  viktoriia-fomina

  committed
  c8cb725

  Copy full SHA for c8cb725

• Run KPrimalDualMaxRes solver for corectness check

  viktoriia-fomina

  committed
  8670b7f

  Copy full SHA for 8670b7f

• Update MaxSAT tests for multiple solvers

  viktoriia-fomina

  committed
  664b0e6

  Copy full SHA for 664b0e6

• Update MaxSAT workflow for multiple solvers

  viktoriia-fomina

  committed
  22db2e2

  Copy full SHA for 22db2e2

• Fix a bug with integer overflow

  viktoriia-fomina

  committed
  99a0bc3

  Copy full SHA for 99a0bc3

• Fix integer overflow in solver

  viktoriia-fomina

  committed
  a39e0c0

  Copy full SHA for a39e0c0

• Set up big timeout for MaxSAT tests

  viktoriia-fomina

  committed
  587d9ed

  Copy full SHA for 587d9ed

Commits on May 13, 2024

• Set up new time for MaxSAT tests

  viktoriia-fomina

  committed
  8400f2a

  Copy full SHA for 8400f2a

• Update TestProtocolModel

  viktoriia-fomina

  committed
  dca5430

  Copy full SHA for dca5430

• Fix an error with redeclaration SoftConstraint in ProtocolModel

  viktoriia-fomina

  committed
  cc93a56

  Copy full SHA for cc93a56

• Inherit secrets in called workflow

  viktoriia-fomina

  committed
  ab0931e

  Copy full SHA for ab0931e

• Temporary remove UF and UFLIA form run

  viktoriia-fomina

  committed
  a51a92b

  Copy full SHA for a51a92b

Commits on May 14, 2024

• Merge KMaxSMTStatistics and KSubOptMaxSMTStatistics

  viktoriia-fomina

  committed
  aabef32

  Copy full SHA for aabef32

Commits on May 15, 2024

• Run tests for QF_UF and QF_UFLIA

  viktoriia-fomina

  committed
  a535c7b

  Copy full SHA for a535c7b

• Create Portfolio solver in tests correctly

  viktoriia-fomina

  committed
  f7ec47e

  Copy full SHA for f7ec47e

• Support interruption for MaxSMT

  viktoriia-fomina

  committed
  5972d0d

  Copy full SHA for 5972d0d

Commits on May 17, 2024

• Implement KSolverRunner and KSolverExecutor in order to interact through ProtocolModel

  viktoriia-fomina

  committed
  912e89e

  Copy full SHA for 912e89e

• Run Portfolio is async mode

  viktoriia-fomina

  committed
  7e196e8

  Copy full SHA for 7e196e8

Commits on May 18, 2024

• Update KMaxSMTResult with timeoutExceededOrUnknown

  viktoriia-fomina

  committed
  e75f2ab

  Copy full SHA for e75f2ab

• Update protocol models etc for timeoutExceededOrUnknown support

  viktoriia-fomina

  committed
  7473769

  Copy full SHA for 7473769

• Descrease test workers number to 1

  viktoriia-fomina

  committed
  e353380

  Copy full SHA for e353380

• Update models to use two lists instead of List<SoftConstraint>

  viktoriia-fomina

  committed
  dcb1b7d

  Copy full SHA for dcb1b7d

Commits on May 19, 2024

• Fix a bug with initializing KPrimalDualMaxResSolverBase in KSolverWorkerProcess

  viktoriia-fomina

  committed
  c7f6f41

  Copy full SHA for c7f6f41

• Add elapsed time to general stat

  viktoriia-fomina

  committed
  9638af4

  Copy full SHA for 9638af4

• Update statistics collection in script

  viktoriia-fomina

  committed
  faadc62

  Copy full SHA for faadc62

• Remove redundant else

  viktoriia-fomina

  committed
  9f869c8

  Copy full SHA for 9f869c8

Commits on May 20, 2024

• Update predicate for checkSubOptMaxSMT in KPortfolioSolver

  viktoriia-fomina

  committed
  c759217

  Copy full SHA for c759217

• Fix Portfolio

  viktoriia-fomina

  committed
  31f65a7

  Copy full SHA for 31f65a7

• Implement native z3 tests

  viktoriia-fomina

  committed
  b729853

  Copy full SHA for b729853

• Set an algorithm for Z3 native

  viktoriia-fomina

  committed
  5a4bb77

  Copy full SHA for 5a4bb77

• Run Z3 native on CI

  viktoriia-fomina

  committed
  ff69d4c

  Copy full SHA for ff69d4c

• Updare solver enum for Z3_Native support

  viktoriia-fomina

  committed
  ed462d3

  Copy full SHA for ed462d3

• Fix compilation

  viktoriia-fomina

  committed
  8062b71

  Copy full SHA for 8062b71

• Update statistics analyzer

  viktoriia-fomina

  committed
  2855eff

  Copy full SHA for 2855eff

• Fix compilation

  viktoriia-fomina

  committed
  29d283e

  Copy full SHA for 29d283e

• Update default value in workflow

  viktoriia-fomina

  committed
  d427dc3

  Copy full SHA for d427dc3

• Update default value in workflow

  viktoriia-fomina

  committed
  cc1441b

  Copy full SHA for cc1441b

• Fix setting solver in workflow

  viktoriia-fomina

  committed
  7788f68

  Copy full SHA for 7788f68

• Add MaxSMTCallStatistics to Z3Native

  viktoriia-fomina

  committed
  0d55a16

  Copy full SHA for 0d55a16

• Add to test stat timeoutExceededOrUnknown option

  viktoriia-fomina

  committed
  5d7cddb

  Copy full SHA for 5d7cddb

Commits on May 23, 2024

• Wrap Yices into SymFpu in tests

  viktoriia-fomina

  committed
  8dd2dc5

  Copy full SHA for 8dd2dc5

• Add symfpu dependency to tests

  viktoriia-fomina

  committed
  b85b2f3

  Copy full SHA for b85b2f3

• Hardcode test data revision

  viktoriia-fomina

  committed
  657a4e7

  Copy full SHA for 657a4e7

• Let Yices-SymFpu run on FP

  viktoriia-fomina

  committed
  d1fcfb5

  Copy full SHA for d1fcfb5

Commits on May 27, 2024

• Update benchmark tests solver list

  viktoriia-fomina

  committed
  1e51545

  Copy full SHA for 1e51545

• Run Yices on corresponding theories

  viktoriia-fomina

  committed
  bca994a

  Copy full SHA for bca994a

Commits on May 28, 2024

• Set up suboptimal mode for Z3 native

  viktoriia-fomina

  committed
  8daaae1

  Copy full SHA for 8daaae1

Commits on May 29, 2024

• Set timeout to 1s

  viktoriia-fomina

  committed
  2dbee6e

  Copy full SHA for 2dbee6e

• Downgrade timeout to 500 ms

  viktoriia-fomina

  committed
  3d8e9de

  Copy full SHA for 3d8e9de

Commits on Jun 14, 2024

• Remove useless NotImplementedException

  viktoriia-fomina

  committed
  1c1f60a

  Copy full SHA for 1c1f60a

• Remove useless maxSMTSuceeded from KMaxSMTResult

  viktoriia-fomina

  committed
  1576cf4

  Copy full SHA for 1576cf4

• Remove useless timeoutExceeded method

  viktoriia-fomina

  committed
  78fcf85

  Copy full SHA for 78fcf85

• Refactor

  viktoriia-fomina

  committed
  3d2a15a

  Copy full SHA for 3d2a15a

• Split checkMaxSMT and checkSubOptMaxSmt (part1)

  viktoriia-fomina

  committed
  e0e6689

  Copy full SHA for e0e6689

Commits on Jun 15, 2024

• Refactor Portfolio: split CheckMaxSMT and CheckSubOptMaxSMT

  viktoriia-fomina

  committed
  070cbcb

  Copy full SHA for 070cbcb