Nonlin LA preds by BritikovKI · Pull Request #790 · usi-verification-and-security/opensmt

BritikovKI · 2024-10-29T15:16:19Z

Allows to create nonlin functions

Removed all of the constraints for the creation of nonlin predicates inside of the functions.
Only the assertions are checked for nonlinearity

aehyvari · 2024-11-04T09:33:26Z

The code fails with this input

(set-logic QF_LIA)
(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
(assert (= (uninterp_mul 1 2) 0))
(check-sat)
(exit)

Here's the output:

(error "Divisor must be constant in linear logic")

(error "define-fun returns an unknown sort")

(error "Unknown symbol `uninterp_mul Int Int'")

(error "assertion returns an unknown sort")

sat

src/itehandler/IteToSwitch.cc

src/logics/ArithLogic.cc

src/logics/ArithLogic.h

src/logics/Logic.h

test/regression/base/arithmetic/miniexample2.smt2

test/unit/test_ArithLogicApi.cc

test/unit/test_Rewriting.cc

aehyvari · 2024-11-04T10:18:20Z

For our limited form of axioms this might actually be just enough. One thing is missing before I can put this to our production: To be sure that we're running the correct version, I'd need to have the version information from opensmt. See issue #800 .

BritikovKI · 2024-11-05T13:59:36Z

Ok, I think generally PR is over

Though, we definitely need some sort of error handling, LANonLinearException produces errors with different format under different complilers rn. Should it be a different issue though?

src/logics/ArithLogic.h

src/logics/ArithLogic.cc

src/tsolvers/lasolver/LASolver.cc

blishko

Some more comments.

src/api/MainSolver.cc

src/logics/ArithLogic.h

blishko · 2024-12-13T13:22:25Z

src/logics/ArithLogic.cc

+            assert(logic.isPlus(polyTerm) || logic.isTimesNonlin(polyTerm));
            for (PTRef factor : logic.getPterm(polyTerm)) {
-                auto [var, c] = logic.splitTermToVarAndConst(factor);
+                auto [var, c] = logic.splitPolyTerm(factor);


Nonlinear multiplication should be handled as a factor, not as a sum, no? I think this is not correct.

In this case it is the same though.. Operations like
x1 * x2 * x3
and
x1 + x2 + x3
Are split in the same manner, elements of the arithmetic operation extracted one by one and analyzed separately

Or maybe I don't fully understand what toPoly function does, but from what I get it splits operation into terms

Can @blishko comment on this? I am not following up on the issue at the moment.

I am also confused right now. How is the term like5 * x1 * x2 gonna be represented?
One nonlinear multiplication with three children, or like 5 * (x1*x2) so the top-level multiplication is linear and the second one is nonlinear?

src/tsolvers/lasolver/LASolver.cc

blishko · 2024-12-13T13:32:57Z

src/tsolvers/lasolver/LASolver.cc

-        assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));
+        auto [v,c] = logic.splitPolyTerm(expr);
        x = getLAVar_single(v);
+        assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));


Why has the assert moved? Just keep it in the original place, no?

It was moved because getLAVar_single contains check for nonlin multiplication and will throw exception if it is detected. Otherwise assertion will fail because v is nonlin multiplication and is not in the scope of assertion...

I can either change assertion disjunction or add handling of the nonlin multiplication before the assertion, but those are both non-perfect solutions either... Tell me which one you prefer!

I do not understand. Since expr must be either NumVar or TimesLin, how can splitPolyTerm(expr) yield TimesNonLin? I would expect that getLAVar_single never throws here. I do not even consider it necessary to add assert(not isTimesNonLin(v)) because I really do not see a rationale for how it could appear here unless I am missing something.

Problem is that at this point expr can be potentially timesNonlin, since we don't have NonLinArith and send potentially Nonlin queries into the LASolver (we can truly understand if it is Lin or Nonlin only after simplifications).
splitPolyTerm is general call, that works both for linear and nonlinear terms...

We are talking about an if block guarded by the condition if (logic.isNumVar(expr) || logic.isTimesLin(expr)), hence why I assume that it is impossible that expr is TimesNonlin.

It is due to our representation of formulas

basically 2xy is (TimesLin 2 (TimesNonlin x y))
Therefore this check doesn't check that there is no nonlin multiplication in the formula

OK. Then I would add an additional assert before getLAVar_single that considers nonlin as well, to 1) make it more under control and 2) to document that this is the expected behavior.

src/common/NonLinException.h

src/logics/ArithLogic.h

src/symbols/SymStore.h

src/symbols/SymStore.cc

src/symbols/SymStore.h

src/symbols/SymStore.cc

src/tsolvers/lasolver/LASolver.cc

Tomaqa · 2025-03-17T10:02:03Z

src/tsolvers/lasolver/LASolver.cc

@@ -91,9 +92,7 @@ void LASolver::isProperLeq(PTRef tr)
    assert(logic.isLeq(tr));
    auto [cons, sum] = logic.leqToConstantAndTerm(tr);


Suggested change

auto [cons, sum] = logic.leqToConstantAndTerm(tr);

[[maybe_unused]] auto const [cons, sum] = logic.leqToConstantAndTerm(tr);

I would also change the name of the function to assertIsProperLeq with [[maybe_unused]] PTRef tr

Should we address it in this PR? Because it already seems to be grown out of scope significantly, and refactoring [cons,sum] is not connected directly to the NonLin support...

Tomaqa · 2025-03-17T10:02:15Z

src/tsolvers/lasolver/LASolver.cc

-    assert(!logic.isTimes(sum) || ((logic.isNumVar(logic.getPterm(sum)[0]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[1]))) ||
-                                   (logic.isNumVar(logic.getPterm(sum)[1]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[0])))));
+    assert(logic.isPlus(sum) or logic.isTimesLin(sum) or logic.isMonomial(sum));
    (void) cons; (void)sum;


Suggested change

(void) cons; (void)sum;

Same question as above, I can do it in separate PR

Tomaqa · 2025-03-17T10:07:33Z

src/tsolvers/lasolver/LASolver.cc


 LVRef LASolver::getLAVar_single(PTRef expr_in) {
-
+    if (logic.isTimesNonlin(expr_in)) { throw NonLinException(logic.pp(expr_in)); }


Can we do a function for this? Like logic.checkIsNotNonlin. Then, for example, changing the error message would be necessary to update in just one place.

Do you mean logic.checkIsNotNonlin would be the only function to throw NonLinException, right?
(Because otherwise it wouldn't bring much benefit...)
However, it would mean making it void, because if/else branch wouldn't make much sense and just calling it within a function to check if it will throw exception or not
I'm not sure how efficient this architectural change would be 🤔

src/symbols/SymStore.h

Tomaqa · 2025-10-24T16:03:27Z

src/symbols/SymStore.cc

+SymRef SymStore::newSymbImpl(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                             bool isInternal) {


After I studied a bit Symbol.h, I believe we should integrate an internal flag into SymbolConfig (e.g. similarly to isInterpreted) instead of this isInternal parameter. This would be compatible with the existing code, allowing to use it also with declareFun etc. Connected to this, I think we should remove SymConf and instead allow graceful construction of SymbolConfig, possibly also adding some getters. For example, I see that noScoping implies isInterpreted (I dunno why, though).

That part of the code is very much historical, to put it nicely. noScoping would probably mean that the symbol is a reserved word. that could well be the reason why it's isInterpreted. I'm not convinced that the choices I made when introducing those fields were very informed. I encourage you to look at them with a critical eye.

@Tomaqa do you think it should be done within the scope of this PR or separately?
Bc it will require slight amount of changes in SymbolConfig

BritikovKI force-pushed the nonlin-la-preds branch 8 times, most recently from d89fbf6 to b1f40d9 Compare October 31, 2024 11:43

BritikovKI marked this pull request as ready for review October 31, 2024 15:09

BritikovKI force-pushed the nonlin-la-preds branch from b1f40d9 to b300ed9 Compare October 31, 2024 15:10

blishko reviewed Nov 4, 2024

View reviewed changes

BritikovKI force-pushed the nonlin-la-preds branch from c0605cd to 78b01bc Compare November 4, 2024 10:11

BritikovKI force-pushed the nonlin-la-preds branch 3 times, most recently from 46d12d9 to 8acd08a Compare November 4, 2024 10:25

BritikovKI linked an issue Nov 4, 2024 that may be closed by this pull request

Opensmt rejects non-linear integer arithmetic too eagerly #655

Open

BritikovKI force-pushed the nonlin-la-preds branch 11 times, most recently from 2810c10 to 32f3743 Compare November 5, 2024 13:51

BritikovKI force-pushed the nonlin-la-preds branch from 00adce9 to c34e1ba Compare November 29, 2024 09:08

blishko requested changes Nov 29, 2024

View reviewed changes

src/logics/ArithLogic.h Outdated Show resolved Hide resolved

src/logics/ArithLogic.cc Show resolved Hide resolved

src/logics/ArithLogic.cc Outdated Show resolved Hide resolved

src/tsolvers/lasolver/LASolver.cc Outdated Show resolved Hide resolved

BritikovKI force-pushed the nonlin-la-preds branch 5 times, most recently from 7e441a2 to adaea42 Compare November 29, 2024 16:59

BritikovKI mentioned this pull request Dec 2, 2024

Implement handling of nonlin Real division #816

Open

BritikovKI requested a review from blishko December 2, 2024 14:44

blishko reviewed Dec 13, 2024

View reviewed changes

Tomaqa reviewed Feb 19, 2025

View reviewed changes

BritikovKI force-pushed the nonlin-la-preds branch 3 times, most recently from c974f2b to 469252e Compare February 27, 2025 13:25

BritikovKI force-pushed the nonlin-la-preds branch from 0a88022 to 469252e Compare March 11, 2025 09:12

Tomaqa self-requested a review March 17, 2025 10:01

Tomaqa reviewed Mar 17, 2025

View reviewed changes

Tomaqa self-requested a review October 24, 2025 15:24

Tomaqa reviewed Oct 24, 2025

View reviewed changes

src/symbols/SymStore.h Outdated Show resolved Hide resolved

Tomaqa reviewed Oct 24, 2025

View reviewed changes

BritikovKI force-pushed the nonlin-la-preds branch from 469252e to d025b20 Compare December 5, 2025 15:30

NonlinWork: old implementation

e93681e

BritikovKI force-pushed the nonlin-la-preds branch from d025b20 to 1c3a5b8 Compare December 5, 2025 15:59

NonlinWork: working rebase to master

3eccfcd

BritikovKI force-pushed the nonlin-la-preds branch from 20f734b to 3eccfcd Compare December 5, 2025 16:05

BritikovKI added 3 commits December 7, 2025 15:32

NonlinWork: Few Comment fixes

2a65984

NonlinWork: fix of clang-format

b1d957d

NonlinWork: NonLin check as a function

3394533

BritikovKI force-pushed the nonlin-la-preds branch from aa4fd8e to 3394533 Compare December 9, 2025 12:00

BritikovKI requested a review from Tomaqa December 9, 2025 12:01

		@@ -91,9 +92,7 @@ void LASolver::isProperLeq(PTRef tr)
		assert(logic.isLeq(tr));
		auto [cons, sum] = logic.leqToConstantAndTerm(tr);

	auto [cons, sum] = logic.leqToConstantAndTerm(tr);
	[[maybe_unused]] auto const [cons, sum] = logic.leqToConstantAndTerm(tr);


		LVRef LASolver::getLAVar_single(PTRef expr_in) {

		if (logic.isTimesNonlin(expr_in)) { throw NonLinException(logic.pp(expr_in)); }

		SymRef SymStore::newSymbImpl(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
		bool isInternal) {

Comments

Conversation

BritikovKI commented Oct 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Allows to create nonlin functions

Uh oh!

aehyvari commented Nov 4, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aehyvari commented Nov 4, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

BritikovKI commented Nov 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

blishko left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

BritikovKI commented Oct 29, 2024 •

edited

Loading

aehyvari commented Nov 4, 2024 •

edited

Loading

aehyvari commented Nov 4, 2024 •

edited

Loading

BritikovKI commented Nov 5, 2024 •

edited

Loading

BritikovKI Dec 9, 2025 •

edited

Loading